Litex: Simply Scale Formal Reasoning In AI Era version v0.1.10-beta (not yet ready for production use)
Jiachen Shen and The Litex Team
Litex: The First Formal Language Learnable in 1–2 Hours
Simplicity is the ultimate sophistication.
– Leonardo da Vinci
Litex(website) is a simple, intuitive, and open-source formal language for coding reasoning (Star the repo!). It ensures every step of your reasoning is correct, and is actually the first reasoning formal language (or formal language for short) that can be learned by anyone in 1–2 hours, even without math or programming background.
Making Litex intuitive to both humans and AI is Litex's core mission. This is how Litex scales formal reasoning: by making it accessible to more people, applicable to more complex problems, and usable by large-scale AI systems. These benefits stem from Litex's potential to lower the entrance barrier by 10x and reduce the cost of constructing formalized proofs by 10x, making formal reasoning as natural as writing.
Here is a comparison between Litex and traditional formal language Lean.
Litex Lean 4 let 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) = 2 * 10 - 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₈⟩
Even Kids can formalize the multivariate equation in Litex in 2 minutes, while it require an experienced expert hours of work in Lean 4. It is a typical example of how Litex lowers the entrance barrier by 10x, lowers the cost of constructing formalized proofs by 10x, making formalization as easy and fast as natural writing. No foreign keywords, no twisted syntax, or complex semantics. Just plain reasoning.
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:
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. 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.
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!
Special Thanks
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 owe special thanks to my friend Zhaoxuan Hong, who built Litex’s powerful toolchains and has supported the project from the very beginning. I am also 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 for their invaluable contributions. I am certain this list of special thanks will only grow longer in the future.