Litex: The First Formal Language Learnable in 1-2 Hours Version: v0.1.10-beta (not yet ready for production use) Author: Jiachen Shen and The Litex Team --- Overview Litex is a simple, intuitive, and open-source formal language designed for coding reasoning efficiently. It aims to: Ensure every reasoning step is correct. Be learnable by anyone within 1-2 hours, no matter their programming or math background. Make formal reasoning accessible and scalable for both humans and AI. Lower the entry barrier and reduce the cost of constructing formalized proofs by 10x. Litex combines ease of learning with formal rigor, making formalization as natural as writing. --- Comparison with Lean 4 Litex simplifies complex formal proofs significantly compared to traditional languages like Lean 4. Example: Solving a system of linear equations Litex syntax example: Lean 4 requires many explicit proof steps and tactics, often several hours for experts. This illustrates how Litex dramatically lowers the time and complexity required for formal reasoning. --- Resources and Community Litex thrives with a growing ecosystem and supportive community. For Litex Users: Official website: litexlang.com — Tutorials, cheat sheets, examples, documentation. Online tutorial: Litex Introduction Cheat sheet: Litex Cheatsheet Download and run Litex locally: Getting Started Contribute to the active development of Litex standard library Python interface: pylitex Community chat: Zulip Contact via email: litexlang@outlook.com For AI Researchers: Litex achieves 100% accuracy on the gsm8k dataset without training: litex-gsm8k-killer Datasets on Hugging Face Powerful Litex Agent: litex-agent Litex LLM Dev project for AI collaborations: litex-llm-dev All repositories are open-source under Apache-2.0 License: https://github.com/litexlang/golitex/blob/main/LICENSE --- Repository Information Stars: 327 Forks: 4 Watchers: 2 Main language: Go (99.5%) Secondary language: Python (0.5%) Commits: 3,978 Latest release: 0.1.11-beta (Aug 21, 2025) Repository structure includes core directories such as: ast, cmp, datacleaner, environment, examples, executor glob, kernellitex_code, number, parser, pipeline, sys, verifier Key files like .gitignore, LICENSE, README.md, go.mod, main.go Visit the repository on GitHub: https://github.com/litexlang/golitex --- Special Thanks Litex creator Jiachen Shen acknowledges many contributors and collaborators including: Zhaoxuan Hong (toolchains) Siqi Sun, Wei Lin, Peng Sun, Jie Fu, Zeyu Zheng, Huajian Xin, Zijie Qiu, Siqi Guo, Haoyang Shi, Chengyang Zhu, Chenxuan Huang Litex mascot: "Little Little O," a curious baby bird full of wonder. --- Summary Litex is a user-friendly formal language designed for rapid learning and scalable formal reasoning, targeting both humans and AI developers. It offers a significantly