From geometric intuition
to verifiable proofs
Learn how to use MechGeo and what each stage of the process actually establishes.
A proof in three steps
- Describe the problem
Write the assumptions and the conclusion in English or Chinese. Name each point and line, and specify relationships such as midpoints, perpendicularity, and parallelism.
- Review the formalization
Check that the generated GeoIR and Lean theorem accurately express your problem. Edit the GeoIR and validate it again if needed.
- Confirm and prove
Confirm the statement to start the automated prover. When it finishes, review the kernel checks, full Lean source, and a plain-language explanation.
Who generates, and who verifies?
Language models translate natural language into formal statements and search for candidate proofs. Their output is not automatically trustworthy. The final proof is checked by the Lean 4 kernel. A result is marked as proved only if it compiles, contains no sorry, preserves the statement, and uses only allowed axioms.
Successful formalization means Lean can understand the statement. A successful proof means the statement has a proof term that passes kernel checking.
A readable intermediate representation
GeoIR sits between natural language and Lean, making translation errors easier to spot. It describes points, constructions, assumptions, and the goal.
point A; point B; point C;
let D = midpoint A B;
let E = midpoint A C;
prove (parallel D E B C)After editing GeoIR, regenerate and check the Lean statement. Previous confirmations and proof results are invalidated.
Understanding proof results
The proof file is accepted by the current Lean environment.
The proof contains no unfinished proof placeholders.
The prover has not changed the statement to be proved.
The proof relies only on allowed foundational axioms.
The plain-language explanation is generated from the verified Lean proof after proving succeeds. It helps you understand the argument; the Lean result remains the basis for verification.
Current limitations
- This is an early research preview. Not all solid geometry problems or complex constructions are supported.
- Natural language can be ambiguous. Review the formal statement carefully before starting a proof.
- Automated proof search may fail or time out. Failure does not mean the statement is false.
- Tasks may queue during busy periods, and each proof has resource limits.
Security and privacy
The proof agent runs in a restricted sandbox with network access disabled and writes limited to the current task workspace. Do not include passwords, API keys, unpublished research data, or other sensitive information in your problem.