Litex: A Simple Formal Language Learnable in 2 Hours

For Verifiable Intellectual Discovery in AI Age

version v0.2-beta (not yet ready for production use)
Jiachen Shen and The Litex Team

What is Litex?

Simplicity is the ultimate sophistication.

– Leonardo da Vinci

Litex is a simple and intuitive open-source computer language for mathematical proofs. It aims to express mathematics as code with verified correctness while staying as close to natural language as possible. Think of it as an eye-opening exploration of finding what mathematics is! (Github, Official Site)

Formal code written in Litex is typically 2-10x simpler than traditional formal languages, and even high-school students (instead of just math PhDs) can understand it. Much lower barrier to entry means Litex could be a game changer for people without PhD-level math background, ranging from AI researchers and scientists to engineers and math-lovers.

Here is an example of how Litex code looks like:

Litex

Lean 4

forall x R, y R:   2 * x + 3 * y = 10   4 * x + 5 * y = 14   =>:     2 * (2 * x + 3 * y) = 2 * 10 = 4 * x + 6 * y     y = (4 * x + 6 * y) - (4 * x + 5 * y) = 20 - 14 = 6     2 * x + 3 * 6 = 10     2 * x + 18 - 18 = 10 - 18 = -8     x = (2 * x) / 2 = -8 / 2 = -4

import Mathlib.Tactic example (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₈⟩

Here is a thorough collection of comparison between Litex and Lean: Litex vs Lean Set Theory Examples. Visit our website for more details. Dataset on Hugging Face is also available.

How Litex Works

Mathematics is nothing more than a game played according to certain simple rules with meaningless marks on a paper.

— David Hilbert

Litex achieves its simplicity by imitating how people reason and how mathematics works. Litex is based on set theory. It searches for known facts mechanically and effectively to prove new facts for you. The user no longer has to memorize and recall known facts and inference rules by hand. Each Litex statement has and only has some of the following 4 effects: define, verify, memorize and infer, which is printed out in the output, making the user easy to know how the proof process works.

Among the 4 effects, verification is the most important one. Litex uses match and substitution to use forall facts to verify the correctness of the statements. It's impossible to explain how it works in a few words. So we put an example here. When forall x human => $intelligent(x) is already stored in memory and Jordan $in human is also stored in memory, when the users type $intelligent(Jordan), Litex will substitute Jordan with x in the statement forall x human => $intelligent(x) and check if the statement is true. If it is, the statement is verified.

Think of this: when the user inputs a fact with proposition name intelligent, Litex will search all known facts with proposition name intelligent (including forall facts like forall x human => $intelligent(x) and specific facts like $intelligent(Jordan)) and check if the given fact matches the known fact. If matched, then it is correct. It works like ctrl+f in your browser. The reason why Lean cannot do this is that Lean can pass prop as forall parameter, so its search space is the whole memory, instead of the memory of the current proposition.

Even for 10-year-old beginners, Litex is straightforward to learn and use. Visit our How Litex Works for more details.

Resources And Community

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:

1. Our official website contains tutorials, cheat sheets, examples, documentation, collaboration opportunities, and more for Litex. All documents on our website are open-sourced here
2. Use pylitex to call Litex in Python
3. Our Community is on Zulip!
4. Email us here.
5. Congratulations! Litex achieves top 10 on Hacker News on 2025-09-27!!
6. Our organization's Github is here. The kernel is here.
7. Our dataset on Hugging Face is here.

References

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:

1. Avigad Jeremy: Foundations https://arxiv.org/abs/2009.09541
2. Terence Tao: Analysis I Fourth edition, 2022. https://terrytao.wordpress.com/books/analysis-i/
3. Weyl Hermann: Philosophy of Mathematics and Natural Science https://www.jstor.org/stable/j.ctv1t1kftd
4. Bertrand Russell: Introduction to Mathematical Philosophy https://people.umass.edu/klement/imp/imp.pdf
5. David Hilbert: Foundations of Geometry https://math.berkeley.edu/~wodzicki/160/Hilbert.pdf

AI references:

1. DeepSeek-R1: Boosting Reasoning Capability in LLMs via Reinforcement Learning
2. AlphaGeometry: An Olympiad-level AI system for geometry
3. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

Special Thanks

巴黎挺好，未来一定更好。未来没有计划，但一定更好。

- 樊振东在巴黎奥运会后接受采访时说

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, Chenxuan Huang, Yan Lu, Sheng Xu, Zhaoxuan Hong, Lei Bai, Xiuyuan Lu, Yunwen Guo for their emotional support and insightful advice. I am certain this list of special thanks will only grow longer in the future.