在依赖项目上下文的Lean 4定理证明中，失败证明过去被当作最终筛选结果丢弃，独立采样让后续尝试几乎从头开始。这套搜索框架让通用推理模型与Lean专用证明器各出一个候选，用编译器错误做两两比较选出当前最佳证明，只在比较判定更好时接受修订，停滞则重新采样。在miniCTX-v2的七个真实Lean 4项目上，pass@32预算内平均通过率比两个基座模型的平均pass@32高12.8个百分点，LLM调用减少21.9%。
通用大模型写几何证明时，先检索结构相似、证明已知的旧题作为示例，再由符号验证器逐轮指出错误，完整流程在FormalGeo-7k的50道SAT级欧氏几何题上把证明正确率提到68%–96%，而既不用类比检索也不用验证器反馈的基线为10%–44%。在同样带验证器反馈、同样推理预算下，仅加入类比引导就把GPT-5从88%提到96%、o1从52%提到80%。
HybridProver把整段证明生成与逐步策略生成接在同一条流水线上：整段模型先给出候选证明，未通过Isabelle检查的候选被抽成保留高层结构的证明骨架，再由策略模型与Sledgehammer逐个子目标补全。在Isabelle版miniF2F的244道测试题上，该流程取得73.8%的成功率，高于此前Isabelle系统的最好成绩61.9%。两个7B规模模型经监督微调与以Isabelle验证为奖励的强化学习训练，说明轻量模型也能生成Isabelle/HOL证明。
这篇综述系统梳理了 AI for Mathematics（AI4Math）的进展、挑战与前景，将研究分为面向特定问题的建模（引导直觉、构造反例、封闭系统形式推理）与通用建模（自然语言推理、形式推理、数学信息检索）两条互补路线，并报告了作者自建的 PKU 本科与博士资格考试评测：GPT-4 平均分低于 60，而 o1、DeepSeek-R1、o3-mini、Gemini 2.5 Pro 等推理增强模型多数超过 90，o3-mini 在 58 道博士资格考试题上平均 84.4 分，同时指出研究级数学仍是开放难题。
已读完全部报道