上海人工智能实验室和复旦大学的研究团队近日开源了 Litex——一门专为降低形式化推理门槛而设计的极简语言。该项目致力于解决传统形式化语言（如 Lean、Coq）学习曲线陡峭的问题，使任何背景的开发者都能够在 1-2 小时内掌握基本的形式化证明编写能力，而非传统的 3-6 个月学习周期。
在过去的一年里，Litex 在开源社区引起了持续关注。上周，该项目登上 Hacker News 全球趋势榜前十，引发了大量开发者围绕形式化语言可用性展开讨论。这一关注度背后，反映的是形式化验证技术在 AI 推理领域日益凸显的重要性。
当前，从 DeepSeek-R1 到 Alpha-Proof 等顶级推理模型都在采用形式化语言来确保推理过程的可验证性。这意味着 AI 系统不仅需要给出答案，还要能够提供严格的推导证明。然而，现有形式化语言的高学习成本成为了技术普及的主要障碍——即使是经验丰富的程序员，也往往需要数月时间才能熟练编写形式化证明。
Litex 的设计目标是让形式化推理过程变得如同编写数学算式一般自然。通过简化语法和概念模型，该项目有望显著降低构建形式化数据集的成本，从而加速这一领域的研究进展。目前，Litex 已在 GitHub 开源，并吸引了来自全球的开发者参与贡献。
图1：Litex项目在Hacker News全球趋势榜上排名前十，显示了国际开发者社区对Litex的高度关注
试想一下，即使是10岁的小朋友，也能直觉地理解数学推理是怎么回事，也能进行简单的数学推理并读懂他人的推理。他们也可以阅读福尔摩斯，理解他探案的思路。人类的推理过程，被数学家证明是可以代码化的。写成代码的数学语言，被称为形式化语言。形式化语言作为推理逻辑最直白、最简洁的表达方式，理应比用自然语言来描述推理过程更加高效。
Litex致力于在1-3年内成为AI推理的基础设施，通过降低门槛让形式化推理从专家级技术变为普及级工具，提升效率将数据构建成本降低10倍加速AI推理能力发展。
技术背景：AI推理的"最后一公里"难题
图2：Litex官方Logo，体现了简洁直观的设计理念
强化学习让 AI 能与自己对弈，并以胜负作为奖励不断提升；同样的方法也可以用于“自出题、自解题”，借助形式化语言提供的绝对精准奖励来增强解题能力。由此可见，形式化语言有望加速 AI 数学能力、AI推理能力的突破，迎来属于它的 AlphaGo 时刻。在强化学习之外，大模型在自然语言理解和生成方面取得了显著进展，但在需要严格逻辑推理的数学和科学计算领域，仍然存在准确性和可解释性的挑战，因此对形式化语言也有很大需求。
然而，现有的形式化语言如Lean、Coq等存在一个根本性问题：学习门槛极高。即使是经验丰富的程序员，也需要花费数月时间才能掌握这些语言的基本用法。这严重限制了形式化推理技术的普及和应用。
Litex的技术创新：从"翻译"到"直觉"
Litex的核心创新在于其设计哲学的根本转变。传统形式化语言要求用户将数学思维"翻译"成复杂的语法结构，而Litex则追求与人类数学直觉的"零差异"表达。传统形式化语言学习需要3-6个月，而Litex学习需要1-2小时。
技术对比：直观性革命
让我们通过一个具体的数学问题来对比Litex与传统形式化语言的差异：
问题：求解二元一次方程组
2x + 3y = 10
4x + 5y = 14
Litex实现（2分钟完成）：
对比结果令人震撼：Litex的代码几乎就是数学表达式的直接映射，而Lean需要掌握大量的tactics（如rw、ring、norm_num等）和复杂的类型系统。更多例子欢迎访问Litex官网。
Litex虽然年轻，但已经构建了非常完备的工具链，包括可交互的在线沙盒、LaTeX翻译功能、Python集成等。
在线交互沙盒：
能告诉用户一步步的推理是怎么被Litex验证的。这里的例子是三段论：乔丹是人，人都有智慧，所以乔丹有智慧。可以看到，最后我们问Litex为什么乔丹有智慧，它告诉我们，因为乔丹是人，人都有智慧。
图3：Litex三段论推理演示，展示如何用Litex表达和验证"乔丹是人，人都有智慧，所以乔丹有智慧"的逻辑推理
Python集成：
可以直接在Python中调用。这对AI研究员来说非常方便，因为AI研究员通常使用Python进行数据处理和模型训练。
图4：Litex Python集成演示，展示如何在Python环境中直接调用Litex进行形式化推理
LaTeX翻译功能：
Litex代码甚至能被Litex内核翻译成LaTeX（不借助大模型，用固定的规则）。这对用户接受Litex非常友好。下面是一个例子以及它被翻译成LaTeX后，用户可以看到的展示效果。
图5：Litex在线沙盒演示，展示Litex代码如何自动翻译成LaTeX格式，便于用户理解和分享
设计原则：三大核心特性
Litex的设计围绕三个核心原则展开：
1、直观性（Intuitive）：代码与数学表达式的"零差异"
2、简单性（Simple）：摒弃复杂的语法和语义结构
3、表达力（Expressive）：支持从基础数学到高级抽象的各种推理任务
实际效果验证：数据说话
Litex团队已经通过多个维度的实验验证了其技术优势：
AI推理性能测试
GSM8K数据集上SFT模型准确率达93.5%，显著超越传统方法
用Agent把GSM8k翻译成Litex，成功率100%，无需任何训练
自然语言→Litex翻译准确度检查器，准确率已达98%
核心语言特性
Litex摒弃了传统形式化语言中的复杂概念：
无需掌握have、by、rw、simp、exact等tactics
无需复杂的类型声明和证明策略：这对人类用户非常友好，因为人从小到大学习数学的思考方式，与Litex的书写方式高度一致
直接支持数学表达式的自然书写：这对大模型训练很重要，因为大模型阅读过无数的自然语言文本，而Litex接近自然语言的特性，使得大模型很容易学会Litex并进行推理
行业认可：顶级机构的背书
图6：Litex吉祥物Little Little O，象征着Litex让形式化推理变得简单友好的理念
Litex项目虽然年轻，但已经获得了广泛的行业认可：
GitHub获得512+⭐，关注者来自DeepSeek、字节Seed、蚂蚁数科、清华、北大、港中文、复旦等顶尖机构
CCF(中国计算机协会），蚂蚁数科，联合上海人工智能实验室 举办AIfor formal language比赛，基于Lean语言和Litex语言
相关机构非常看好它在科学探索、可信AI、AI for Math、Math for AI等领域的应用。Litex致力于未来成为AI推理的基础设施，通过构建大规模数学推理数据集和训练专用推理模型，最终打造可信AI生态，让形式化推理从专家级技术变为普及级工具。
Litex采用完全开源策略，欢迎全球开发者和研究者参与。已经开源的项目包括官网上的在线沙盒、教程、语法速查表，Hugging Face上的数据集，GitHub上的内核、标准库、Agent、任务验证器、LLM开发框架等。可以关注Litex的社交媒体账号，获取最新的项目进展和社区动态。
- 官网：https://litexlang.org
- GitHub(欢迎点⭐️支持！)：https://github.com/litexlang/golitex
- 社区: https://litex.zulipchat.com/join/c4e7foogy6paz2sghjnbujov/
- 邮箱：[email protected]
- 小红书: 名字是 Litexlang，id是 27446152057
- B站: 关注 Litexlang
- x.com: Litex@litexlang
