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
... continue reading