ProofSketch：用推理模型自动生成结构化数学证明大纲

ProofSketch项目利用小米MiMo推理模型，将非形式化数学命题转化为结构化证明大纲。核心目标是解决数学证明学习与生成的困境：传统形式化工具（如Lean、Coq）学习曲线陡峭，大语言模型输出不稳定且缺乏结构。通过生成包含策略、步骤、依赖关系和置信度的抽象语法树（AST），ProofSketch让证明过程可审计、可验证，在完全形式化与自由文本之间找到平衡。

数学证明对学习者而言是难点，即使简单命题（如两个偶数之和为偶数）也需严谨的定义理解、策略选择与步骤组织。传统证明辅助工具要求掌握复杂形式化语言，大语言模型生成的证明文本存在输出不稳定、错误隐藏的问题。ProofSketch旨在填补完全形式化与自由文本生成之间的空白。

ProofSketch将证明写作视为推理任务，采用小米MiMo推理模型输出结构化ProofOutline AST而非自由文本。输入为非形式化命题，输出包含6种证明策略（直接证明、归纳法等）、有序步骤列表（带显式依据）、步骤依赖图、未闭合缺口标记及置信度。技术架构为：MiMo生成AST → Python确定性渲染器 → Markdown/JSON输出。

以'两个偶数之和为偶数'为例，ProofSketch生成的大纲采用直接证明策略（置信度0.95）。步骤包括：假设a、b为偶数→依据定义转化为2j和2k→代数运算得2(j+k)→结论为偶数。每个步骤标注依据（如定义、代数定律）和依赖关系，特点是策略明确、步骤有序、依据显式、依赖可视、置信度量化。

与现有工具对比：

特性	GPT-4自由文本	Lean/Coq	ProofSketch
结构化AST	否	是	是
策略选择	是	N/A	是
缺口显式标记	部分	是	是
步骤依据	部分	是	是
学习曲线	低	高	中
ProofSketch定位为中间方案，虽非证明检查器，但显式标记缺口让错误更易发现。

技术实现上，项目用Pydantic定义ProofOutline schema确保格式正确。使用方式包括： 1.命令行工具：支持Markdown/JSON输出； 2.Python库：集成生成大纲； 3.配置MiMo API：通过环境变量设置密钥与模型。模型显式标记未闭合缺口，不隐藏错误。

未来规划包括Lean4 Stub渲染器、步骤依赖图可视化、对抗性检查。总结：ProofSketch通过解构证明过程帮助学习者理解推理逻辑，为数学教育、形式化验证入门及研究者提供易上手的结构化方案，其混合架构为其他AI辅助工具设计提供参考。