litexlang/golitex

解决的问题

Litex 解决了自然数学写作与形式化验证之间的差距。传统的证明助手通常要求用户学习复杂的类型系统编排和与数学家实际解题方式大相径庭的证明脚本。Litex 允许用户以自然、可读的顺序书写数学事实，而机器则负责处理常规的局部推理和验证。

工作原理

Litex 是一种基于集合论的事实导向语言。它通过维护数学对象、定义和事实的已验证上下文来工作。

• 事实匹配：系统通过等式替换、定义和量化规则重建常规推理。
• 证明过程：对于复杂步骤，用户可以使用 witness（用于存在性声明）、obtain（使用现有证词）、by contra（用于矛盾）、by induc（用于归纳）等命令显式定义证明路径。
• 验证：每个被接受的陈述都提供其被接受的原因（例如特定定义或算术规则）以及它为后续步骤提供了什么内容。
• Lean 集成：Litex 可以编译为后端中间表示（IR），然后由 Lean 编译器消费，生成对 Lean 和 Mathlib 载体的语义包装器。

适用人群

• 数学家和学生：希望使用熟悉符号编写可验证数学，但又不想承受传统形式语言陡峭学习曲线的人。
• AI 研究者：开发需要机器可验证局部反馈和明确假设的 AI 修复循环的开发者。
• 教育工作者：希望提供可识别的数学，并立即反馈某个特定事实是否由当前上下文支持的教师。

特色亮点

• 可读语法：使用 LaTeX 风格符号和集合论，使代码接近普通数学写作。
• 事实导向：专注于陈述数学结论，而非手动编码证明替换的机制。
• 可检查验证：提供详细诊断（-detail 模式），并可生成关系图以可视化概念和定理之间的联系。
• Lean 编译路径：提供将高级 Litex 开发转换为 Lean 形式语言的路径。