FORMAL PROOF WORKSPACE

验证一道几何题

描述题目，审阅机器形式化结果，再交由 Lean 内核验证。

01

描述你的几何问题Informal problem

形式化模型选择用于理解题目并生成 GeoIR 的模型

支持中文与英文 · Tab 补全示例题目

02

审阅形式化结果Formal workspace

1Problem2Review3Proof

GeoIR representation

可编辑

修改后需要重新验证

Lean theorem

只读

尚未检查

✓

HUMAN CHECKPOINT

形式化是否准确表达了原题？

确认后，Prover 将锁定当前版本并搜索证明。任何修改都会使本次确认失效。

Kernel verification

运行中

Prover 工作中正在搜索并检查形式证明

00:00

CHECK 01Lean 编译

CHECK 02无 sorry / admit

CHECK 03Statement 未改变

CHECK 04Axiom 检查

Informal solution · 非形式证明

证明完成后生成直观解法。

用于帮助理解；最终可信结果以 Lean 内核检查为准。

Kernel-checked Lean source

Prover execution log

Result JSON