基于 Mathlib 的 Lean 4 形式化项目，将开源代数几何参考书 Stacks Project 转写为机器可验证的证明。
123+19 本周26LeanApache-2.0更新于 昨天
#theorem-proving
2026 年精选开源定理证明工具
定理证明工具用于检查程序或系统设计中性质的形式化证明，通常借助交互式证明器完成。选择时应关注工具面向的逻辑或语言，以及证明工作中有多少由自己编写、多少依靠自动化。LeanCopilot为Lean加入基于大语言模型的策略建议，TorchLean在Lean 4中验证神经网络，tla-ts则是Java编写的TLC模型检查器的TypeScript替代品，可直接替换使用。
共 6 个仓库
用 TypeScript 实现的 TLA+ 解释器与模型检查器，可替代基于 Java 的 TLC，在浏览器、Node 和 Bun 中运行。
237+46 本周10TypeScriptMIT维护活跃更新于 6小时前
基于 Lean 4 的形式化验证框架，可对 C#、F# 等 .NET 语言编译出的 CIL 字节码进行机器可检查的正确性与内存安全证明。
114+10 本周3LeanOther更新于 9小时前
一门用法则与证明约束 AI 生成代码、并可编译为 CPU/GPU 并行程序的编程语言。
2.5万+292 本周797TypeScriptApache-2.0维护活跃更新于 8小时前
为 Lean 定理证明器提供基于大语言模型的证明自动化，包括策略建议、证明搜索和前提选择。
1341+2 本周129C++MIT维护活跃更新于 26天前
基于 Lean 4 的框架，用于神经网络的形式化规约、执行与形式验证，支持形状检查的张量与类 PyTorch 训练。
206+14 本周25LeanMIT维护活跃更新于 10天前