litexlang/golitex

What it solves

Litex addresses the gap between natural mathematical writing and formal verification. Traditional proof assistants often require users to learn complex type-system orchestration and proof scripts that differ significantly from how mathematicians actually solve problems. Litex allows users to write mathematical facts in a natural, readable order while the machine handles the routine local justifications and verification.

How it works

Litex is a set-theory-based, fact-oriented language. It operates by maintaining a checked context of mathematical objects, definitions, and facts.

• Fact Matching: The system reconstructs routine justifications through equality replacement, definitions, and quantified rules.
• Proof Processes: For complex steps, users can explicitly define proof routes using commands like witness (for existential claims), obtain (to use existing witnesses), by contra (for contradictions), and by induc (for induction).
• Verification: Every accepted statement provides evidence of why it was accepted (e.g., a specific definition or arithmetic rule) and what it makes available for future steps.
• Lean Integration: Litex can compile to a backend intermediate representation (IR) which is then consumed by a Lean compiler to emit semantic wrappers over Lean and Mathlib carriers.

Who it’s for

• Mathematicians and Students: Those who want to write checkable math using familiar notation without the steep learning curve of traditional formal languages.
• AI Researchers: Developers building AI repair loops that require machine-checkable local feedback and explicit assumptions.
• Educators: Teachers who want to provide recognizable mathematics with immediate feedback on whether a specific fact is justified by the current context.

Highlights

• Readable Syntax: Uses LaTeX-style notation and set theory to keep the code close to ordinary mathematical writing.
• Fact-Oriented: Focuses on stating mathematical conclusions rather than manually encoding the mechanics of proof replacement.
• Inspectable Verification: Provides detailed diagnostics (-detail mode) and can generate relation graphs to visualize how concepts and theorems are connected.
• Lean Compilation Path: Offers a path to translate high-level Litex developments into the Lean formal language.