标签
菲尔兹奖得主John Pardon表示，AI如今已完全理解他最混乱的数学证明，能发现细微错误，甚至能证明非平凡的结果——这与他仅仅一年前的观点完全相反，他称这一进展对数学而言将改变世界。
LeanPRM提出利用Lean证明助手自动为自然语言数学证明生成步骤级正确性标签，无需人工标注即可训练过程奖励模型（PRM）。Qwen3-4B验证器在该数据上训练后，步骤级标签准确率从48.2提升至74.7，并在IMO级问题的N选优选择和多个外部验证基准上超越使用PRM800K训练的验证器。
OpenAI 一次性发布了近 400 条 AI 生成的数学结果，涵盖 700 多篇手稿，令数学界既震惊又焦虑；但仅约 42% 的成果完成了 Lean 形式化验证，数学家们表示可能需要数年才能消化这批成果。
OpenAI 更新其数学仓库，新增 6 个 Lean 形式化证明、19 项修改，并撤回三项数学结果；仓库约 42% 的核心结果已完成形式化验证，且大部分成果由未发布的内部模型经大量思考计算生成。
Bend是一种快速、并行的编程语言，通过证明机制防止AI出错，专为AI辅助开发而设计，拥有C语言级别的速度和CUDA并行能力。
OpenAI声称发现了一个由AI生成的纳维-斯托克斯方程解，这是一个有200年历史的数学问题，但学术界人士正在争议其归属，并指责OpenAI在得知他们的工作后仓促行事。
RePro将面向Lean的神经自动化定理证明器集成到基准重写中，以确保问题有效性和答案正确性，从而可靠评估LLMs在数学问题求解中的表现。
AdvancedMathBench是一个新的基准套件，用于评估大语言模型在高级数学证明生成与验证方面的性能。它包含用于生成的ProverBench和用于验证的VerifierBench，表明当前模型如GPT-5.5-xhigh仅取得了有限的性能。
来自牛津、剑桥、MIT、CMU等机构的研究人员开展了一项混合方法研究，考察人们如何将AI工具融入数学证明形式化工作流程。研究发现，借助AI辅助时，参与者的形式化准确率普遍更高，同时他们倾向于在证明发现过程中保持人类对高层决策的主导权。
Research Math Agents (RMA) 是一个用于研究级数学问题自动推理的智能体框架，在 First Proof 基准测试中取得最先进结果，解决了10个问题中的8个，优于 GPT-5.2R 和 Aletheia 等强基线。
ProofGrid是一个基准测试套件，通过使用极小形式化符号的机器可验证证明来评估LLM推理，包含证明编写、检查与补全任务，揭示了进展与尚存局限，包括认知不稳定性。