version v0.1.10-beta (not yet ready for production use)
Jiachen Shen and The Litex Team
Simplicity is the ultimate sophistication.
– Leonardo da Vinci
Litex is a simple open-source computer language for mathematical proofs. It aims to express mathematics as code while staying as close to natural language as possible, making it both rigorous and accessible. (Star the repo!) With just one to two hours of learning the fundamentals, you can write code that solves interesting mathematical problems with verified correctness! Litex automatically verifies your proofs and shows you step-by-step how each inference is executed, making the reasoning process transparent and educational.
How does Litex work? It achieves its simplicity by imitating how people reason and how mathematics works. Litex uses a set of axioms (i.e. ZFC axioms and basic logic) and inference rules that are sufficiently expressive to capture mathematical concepts. (axioms + inference rules = math world) Its close-to-natural-language syntax means users often forget they're using a formal language, lowering the barrier of formal reasoning by 10x compared with traditional formal languages. We want to make Litex easy-to-learn even for 10-year-old beginners in mathematical proof and verification.
Official Documentation is our website. Read Tutorial, How Litex Works for more details. Hugging Face Dataset is on Hugging Face.
Our intent was to create a pleasant computing environment (Unix) for ourselves and our hope was that others liked it.
- Dennis Ritchie
| Litex | Lean 4 |
|---|---|
let x R, y R: 2 * x + 3 * y = 10 4 * x + 5 * y = 142 * (2 * x + 3 * y) = 2 * 10 = 4 * x + 6 * yy = (4 * x + 6 * y) - (4 * x + 5 * y) = 2 * 10 - 14 = 62 * x + 3 * 6 = 102 * x + 18 - 18 = 10 - 18 = -8x = (2 * x) / 2 = -8 / 2 = -4 |
import Mathlib.Tacticexample (x y : ℝ) (h₁ : 2 * x + 3 * y = 10) (h₂ : 4 * x + 5 * y = 14) : x = -4 ∧ y = 6 := by have h₃ : 2 * (2 * x + 3 * y) = 2 * 10 := by rw [h₁] have h₄ : 4 * x + 6 * y = 20 := by linear_combination 2 * h₁ have h₅ : (4 * x + 6 * y) - (4 * x + 5 * y) = 20 - 14 := by rw [h₄, h₂] have h₆ : (4 * x + 6 * y) - (4 * x + 5 * y) = y := by ring have h₇ : 20 - 14 = 6 := by norm_num have h₈ : y = 6 := by rw [←h₆, h₅, h₇] have h₉ : 2 * x + 3 * 6 = 10 := by rw [h₈, h₁] have h₁₀ : 2 * x + 18 = 10 := by rw [mul_add] at h₉ simp at h₉ exact h₉ have h₁₁ : 2 * x = -8 := by linear_combination h₁₀ - 18 have h₁₂ : x = -4 := by linear_combination h₁₁ / 2 exact ⟨h₁₂, h₈⟩
|
While Lean 4 is a powerful and rigorous proof assistant ideal, it requires months of training and years of experience to master. Litex takes a different approach: prioritizing accessibility and ease of use, enabling even beginners to formalize naive tasks like multivariate equations in minutes.
Making Litex intuitive to both humans and AI is Litex's core mission. We want people feel happy using Litex. Just like how Python lowers the barrier of programming by 10x compared with C/C++, Litex lowers the barrier of formal reasoning by 10x compared with previous formal languages like Lean.
Since each Litex sentence corresponds directly to an expression in everyday mathematical language, and since it is supported by set theory (ZFC) and basic logic (not, forall, exist, or), Litex does not sacrifice any rigor. So please do not think about Litex using the mindset of traditional formal languages. Instead, imagine yourself as a college student or even a high school student who has a basic understanding of set theory — regardless of whether you like Litex or are skeptical of it.
In summary, Litex is a piece of software that imitates the way people think when they verify mathematics in everyday reasoning, using a small number of straightforward rules.
It’s best to do one thing really, really well.
- Google, ten things we know to be true
Litex is a focused and deeply crafted language. We have invested significant effort in refining and enhancing it. Like other focused and profound products, users naturally find ways to integrate Litex into their own work—this is both inspiring and exciting. Here are some examples of how Litex is used:
Litex For AI
AI pioneer Geoffrey Hinton notes that in mathematics, models operate like in Go or chess—within closed systems with fixed rules, where they can generate their own training data. Formal languages (e.g., Litex) are key to self-improvement because computers can automatically and reliably verify whether mathematical reasoning is correct, enabling effective self-supervised learning.
This is crucial for the following areas:
| Application Area | Examples |
|---|---|
| Model Reasoning | DeepSeek-R1 |
| AI For Math | AlphaProof |
| Safe and Trustful AI | Formal verification of AI systems |
| AI Scientific Exploration | Automated theorem discovery |
Litex For Math
Litex enables automatic verification and large-scale mathematical collaboration. It clarifies dependency structures among complex theorems and transforms mathematical work into mathematical engineering—as intuitive as writing Python code, while maintaining full rigor through ZFC axioms.
Litex For Everyone
Litex is accessible to everyone—from children to experts. With just 1-2 hours of learning, anyone with basic set theory knowledge can write verified proofs. Litex's natural-language-like syntax makes it 10x easier to learn than traditional formal languages, democratizing rigorous mathematical thinking.
The best way to predict future is to create it.
-- Alan Kay
Litex is nothing without its community and technical ecosystem.
Resources for Litex users:
- Our official website contains tutorials, cheat sheets, examples, documentation, collaboration opportunities, and more for Litex. All documents on our website are open-sourced here
- Learn Litex online. A short list of major Litex statements and their usage are shown in the cheat sheet.
- Theory Behind Litex: From a Mathematical Perspective, From a Programming Perspective
- You can run litex on your own computer,start from here
- Litex standard library is under active development. Contribute to it and earn impact rewards!
- Use pylitex to call Litex in Python
- Our Community is on Zulip!
- Email us here.
- Congratulations! Litex achieves top 10 on Hacker News on 2025-09-27!!
Resources for AI researchers who want to develop Litex-based AI systems, mostly developed by the Litex open-source community:
- Litex achieves 100% accuracy on gsm8k dataset without any training Github
- Litex Dataset is on Hugging Face. Contribute to it and earn impact rewards!
- Here is a really powerful Litex Agent Github. It is so powerful that much code in our standard library is generated by it!
- AI researchers interested in Litex might find Litex LLM Dev useful. Contact us if you are interested in collaborating on this project!
All of our repositories are open-sourced. Just issue PRs and tell us any ideas about Litex! Maybe we can build the future together!
If I have seen further [than others], it is by standing on the shoulders of giants.
- Isaac Newton
Although Litex is a very pragmatic language which contains and only contains the proof methods, axioms, keywords, etc. that people need in their daily mathematical work—things that are often so taken for granted that people usually don't even notice them —- it is equally important to note that Litex indeed has gained great conceptual inspiration from the masters.
Mathematics references:
- Avigad Jeremy: Foundations https://arxiv.org/abs/2009.09541
- Terence Tao: Analysis I Fourth edition, 2022. https://terrytao.wordpress.com/books/analysis-i/
- Weyl Hermann: Philosophy of Mathematics and Natural Science https://www.jstor.org/stable/j.ctv1t1kftd
- Bertrand Russell: Introduction to Mathematical Philosophy https://people.umass.edu/klement/imp/imp.pdf
- David Hilbert: Foundations of Geometry https://math.berkeley.edu/~wodzicki/160/Hilbert.pdf
AI references:
- DeepSeek-R1: Boosting Reasoning Capability in LLMs via Reinforcement Learning
- AlphaGeometry: An Olympiad-level AI system for geometry
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
Sometimes it is the very people who no one imagines anything of who do the things that no one can imagine.
– Alan Turing
Litex Mascot: Little Little O, a curious baby bird full of wonder
Hi, I’m Jiachen Shen, creator of Litex. It is so fortunate to receive tremendous help from friends and colleagues throughout this journey of designing, implementing, and growing Litex into a community. Without their support, Litex would not have had the chance to succeed.
I am deeply grateful to Siqi Sun, Wei Lin, Peng Sun, Jie Fu, Zeyu Zheng, Huajian Xin, Zijie Qiu, Siqi Guo, Haoyang Shi, Chengyang Zhu, Chenxuan Huang, Yan Lu, Sheng Xu, Zhaoxuan Hong for their invaluable contributions. I am certain this list of special thanks will only grow longer in the future.
