从几何直觉到
机器可验证的证明
这份文档介绍如何使用 MechGeo，以及系统中每一层结果究竟意味着什么。
三步完成一次证明
- 描述题目
使用中文或英文写出条件和待证结论。明确命名点、直线以及中点、垂直、平行等关系。
- 审阅形式化
检查生成的 GeoIR 与 Lean theorem 是否准确表达原题。必要时编辑 GeoIR 并重新验证。
- 确认并证明
锁定陈述后启动自动证明。完成后可查看内核检查、完整 Lean 源码及直观解法。
谁生成，谁验证？
语言模型负责把自然语言转换为形式陈述，并搜索候选证明。它的输出本身并不自动可信。最终证明会交给 Lean 4 内核检查；只有成功编译、没有 sorry、陈述未改变且公理在允许范围内，才会标记为已证明。
关键边界
“形式化成功”只代表陈述可以被 Lean 理解；“证明成功”才代表该陈述拥有通过内核检查的证明项。
可读的中间表示
GeoIR 位于自然语言和 Lean 之间，便于人类发现题意翻译错误。它描述点、构造、假设和目标。
point A; point B; point C;
let D = midpoint A B;
let E = midpoint A C;
prove (parallel D E B C)修改 GeoIR 后必须重新生成并检查 Lean 陈述，旧的人工确认和证明结果会失效。
理解证明结果
Lean 编译
证明文件能被当前 Lean 环境接受。
无 sorry
没有使用未完成证明占位符。
Statement 未改变
证明器没有改写待证命题。
Axiom 检查
证明仅依赖允许的基础公理。
“直观解法”是在证明成功后，根据已验证 Lean 证明生成的可读解释；它帮助理解，但可信性的最终依据仍是 Lean 结果。
当前限制
- 这是早期研究预览，并非所有立体几何或复杂构造都已覆盖。
- 自然语言可能存在歧义，提交证明前应认真核对形式化陈述。
- 自动证明搜索可能失败或超时；失败不等于命题为假。
- 繁忙时任务可能需要排队，单次证明的资源受到限制。
安全与隐私
证明代理运行在受限沙箱中，网络访问关闭，写入范围限制在当前任务工作区。请不要在题目中提交密码、API Key、未公开研究数据或其他敏感信息。