Litex：用数学事实自证的形式语言，可将证明转交 Lean 复核

实验性数学形式语言 Litex 让用户直接写下想证明的数学事实，由检查器从已有定义和结论中寻找依据，无需像 Lean 那样用 tactic 引导推导。它支持定义、证明、复用与 LaTeX 排版，并能把部分证明和计算定义转成 Lean 代码、Python 或 C99 程序，其中 Lean 集成仍处实验阶段。Litex 的 Rust 核心已超二十万行，项目始于 2024 年，目前仍在探索中。