- 2026
H1 · 历史里程碑核验中
公开仓库包含总览、手稿索引、PDF 与源码、Lean 库与形式化目录、十个精选 reasoning summaries，以及保存公开版本历史的承诺。OpenAI 明确提醒部分未形式化结果可能存在问题， 并表示后续修订将保留历史版本。
openai · advisory-group-on-mathematics-and-artificial-intelligence · openai-internal-math-model · lean · comparator
数学发现 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑核验中
论文的方法部分说明，Anthropic 员工最初让内部研究模型研究一个基于 average-case Zero-k-Clique 的密码学问题。
anthropic · claude · lean · comparator · nanoda
数学发现 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑论文已发布
作者在致谢中明确表示，论文中的大多数证明与数学思想由 ChatGPT 找到；其中 suspension idea 被特别指出为人类作者提出的重要贡献。作者把自己的主要作用描述为理解模型给出的 证明、检查和组织数学内容并改善阐释。
chatgpt
数学发现 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
Meta 表示，人类数学家负责选题并引导研究，另有一组数学家对工作进行审查；每篇论文标记 哪些段落主要由研究者或 AI 起草，并明确引用已有及同期工作。
meta · muse-spark-1-1 · muse-spark-1-2
数学发现 · 证明证据: E2 · 研究记录
H2 · 领域里程碑尚属声明
AGMAI 表示该建议吸收了数学共同体超过 600 份反馈。文件区分两类情形：由负责的数学家 完整理解的普通论文，以及尚无人类完整理解的 AI 输出。
advisory-group-on-mathematics-and-artificial-intelligence · institute-for-advanced-study
领域建构证据: E2 · 研究记录
H2 · 领域里程碑尚属声明
FrenzyMath 报告该项目约包含 320 万行 Lean，LLM 与计算服务器总成本低于 3 万美元。
frenzymath · pku-ai4math · lean · comparator · nanoda
形式化 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
该组织说明，其形成始于 OpenAI 接触部分后来的成员，希望建立外部顾问委员会； 在与 OpenAI 沟通后，这些数学家决定改为成立一个独立组织并邀请其他成员加入。
advisory-group-on-mathematics-and-artificial-intelligence · institute-for-advanced-study · openai
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该档案库有意采用不同于 Mathlib 的定位：它接收可能不适合 Mathlib 高度整合式库结构 的独立完整形式化项目，同时施加自动化维护与质量检查。公开仓库说明，目前项目导入 仍由人类选择，而 AI 系统实质参与审查、维护与优化。
lean-pool · lean · gpt-6-astra · comparator
基础设施 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
FormalFlow 以共享 blueprint 为核心，将长程形式化组织为嵌套的规划、证明与审查循环。 AI Agent 负责实现和审查证明任务，人类则监督整体项目、对照形式化开发与原始数学文本， 并处理语义偏差。
formalflow · lean
形式化 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑部分核验
公开项目提供一篇未署名数学论文、基于 mathlib Liouville 函数的完整 Lean 4 形式化、固定工具链元数据、构建与公理审计以及证明路线检查。另一个独立审计仓库 在 Linux 上重新构建冻结的 v1.0.
gpt-6-astra · lean
数学发现 · 证明证据: E4 · 独立检查
H2 · 领域里程碑尚属声明
该声明形成于一周内围绕 AI 数学能力快速提升和高关注度数学问题求解展开的密集讨论。其核心框架是：企业以 benchmark 和竞赛式突破为导向的激励，可能与数学共同体重视理解、交流、归属、人才培养和长期知识积累的价值发生错位。
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
Magenta 使用 statement judge 检查生成的 Lean 命题是否保持原始非形式问题的含义，并使用 error-attribution judge 判断失败尝试应回到数学推导还是进行局部 Lean 修复。
magenta · lean · k2-horizon-7b
系统 · 形式化证据: E2 · 研究记录
H1 · 历史里程碑部分核验
两位研究者明确将底层强迫爆破研究路线归功于 Diego Córdoba 与 Luis Martínez-Zoroa，并描述其使用 LLM 将该路线从较粗糙的外力条件推进到光滑外力及相关流体方程。
claude · codex · lean · mathlib
数学发现 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑存在争议
OpenAI 表示成功搜索约使用 10,000 个并发 Agent 工作约 88 小时，随后继续进行 Lean 形式化与验证。
openai · openai-internal-model · gpt-6-astra · lean
数学发现 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准覆盖马尔可夫链、更新过程、随机游走、鞅、停时、排队论、布朗运动、随机微积分、弱收敛、泊松过程与连续时间马尔可夫过程。
case-western-reserve-university · stochbench · lean
基准 · 数据集证据: E3 · 可检查工件
H1 · 历史里程碑已有独立佐证
Claude Agent 使用 Anthropic 的 Prove2Me 工作流构建形式化子问题依赖图，并将其扩展为数百万行 Lean 代码。
anthropic · imperial-college-london · lean-community · claude · prove2me · lean · mathlib
形式化 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑核验中
公开的 PrimeGaps186 仓库包含 DHL[40,2] 与 186 素数间隔结论的 Lean 4 开发， 并附带 Python/FLINT 数值 certificate。
openai · gpt-6-astra · lean · comparator · nanoda
数学发现 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
Palomar 的设立背景是 machine-assisted / machine-generated mathematics 数量快速增加， 而成果分散在代码仓库和公告中，外部读者难以核查。
lean-fro · icarm · palomar-registry · lean · comparator · nanoda
基础设施 · 领域建构证据: E3 · 可检查工件
H1 · 历史里程碑已有独立佐证
Claude 协调数十个子 Agent、检索文献并进行数值检查，随后生成论文；Anthropic 数学家审核结果，Lean 形式化通过 comparator。
anthropic · claude-research · lean
数学发现 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑存在争议
OpenAI 表示内部 Astra 模型生成数学论证，人类与模型共同整理稿件，随后模型把每项论证形式化为 Lean certificate。
openai · openai-astra-internal · lean
数学发现 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑部分核验
问题由数学家筛选，并尽可能配套专用计算验证器，同时按解答的重要性进行分级。
epoch-ai · frontiermath-open-problems
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
该试点仅允许使用中间检查点、训练协议和训练数据均公开的模型。6 支团队在 6 道证明题上产出有效提交；AIMO 使用同一专家评分流程，将这些结果与开放权重及商业前沿模型比较，并公开提交内容与详细评分数据。
aimo-prize · xtx-markets · aimo-proof-pilot
竞赛 · 基准证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
该声明源于 2025 年 9 月 Lorentz Center 举办的一次会议，约 60 名参与者来自 10 个国家，背景覆盖数学、计算机科学、哲学、历史、社会科学、产业与政府。随后较小的工作组在数月内结合广泛共同体反馈形成文本。
international-mathematical-union · lorentz-center
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
AlphaProof Nexus 让前沿 LLM 子 Agent 围绕 Lean 编译器工作，并通过专用工具与进化搜索逐级增强证明搜索。
google-deepmind · university-of-texas-at-austin · alphaproof-nexus · lean · gemini
系统 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑已有独立佐证
模型使用代数数论工具发现构造；OpenAI 同时发布证明与由外部数学家撰写的 companion paper，后者检查并解释了论证。
openai · openai-internal-reasoning-model
数学发现 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
SorryDB 抓取符合条件的公开 Lean 仓库，为尚未完成的 `sorry` 命题记录可复现的仓库与工具链坐标，并要求证明系统在原始项目上下文中填补证明缺口。验证器会重建相应项目并检查候选证明，夜间更新的数据库则持续提供新任务。
sorrydb · sorrydb · lean
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑核验中
内部模型在有限人工监督下工作；研究者有时要求重试或澄清，并在人类判断下选择候选尝试。
openai · first-proof · openai-internal-reasoning-model
基准 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
M2F 首先把长篇数学文档翻译为按依赖排序的 Lean 声明骨架，并修复项目层面的结构不一致；随后固定命题签名，利用验证器反馈迭代填补证明缺口。配套 ReasBook 仓库公开了由教材和研究论文生成的形式化项目。
peking-university · m2f · reasbook · lean
形式化 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
Aletheia 将高级 Gemini Deep Think 模型与迭代验证、修订及密集工具使用结合，面向需要文献导航和长证明链的研究环境。作者还明确区分不同自主性与新颖性层级，而非把所有 AI 辅助结果视为同一种贡献。
google-deepmind · aletheia · gemini-deep-think
系统 · 数学发现证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该系统以通用 Coding Agent 循环作为 Lean 工作的控制器，并通过面向 MCP 的接口接入定理检索、非形式证明、验证和辅助推理工具。公开仓库提供安装说明、可运行的 Agent 工具以及 Putnam 形式证明产物。
project-numina · numina-lean-agent · claude-code · numina-lean-mcp · lean
系统 · 证明证据: E3 · 可检查工件
- 2025
H2 · 领域里程碑论文已发布
该论文研究最大似然估计在数据增加时其期望预测误差是否单调改善，证明若干 Gaussian 与 Gamma 情形下的 forward-KL 单调性，并给出适用于广泛指数族的 reverse-KL 论证。OpenAI 将其作为 GPT-5.
openai · gpt-5-2-pro
数学发现 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
GPT-5 提出多个方向和若干关键结构性想法；Ryu 负责检查与重构，并与 Uijeong Jang 写成严格的最终证明。
ucla · openai · gpt-5
数学发现 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该架构生成并形式化有用引理、搜索形式证明，并通过专用组件处理几何。
harmonic · aristotle · lean
证明 · 竞赛证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
系统采用脚手架式数据合成、验证器引导的迭代修复与模型平均。
princeton-university · nvidia · goedel-prover-v2 · lean
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
系统依据 Lean 反馈迭代改进整段证明，并使用深度与广度相结合的测试时搜索策略。
bytedance-seed · seed-prover · seed-geometry · lean
证明 · 竞赛证据: E3 · 可检查工件
H1 · 历史里程碑已有独立佐证
与 2024 年的 AlphaProof 和 AlphaGeometry 2 不同，2025 年系统直接读取官方题目并生成自然语言证明，无需人工翻译成 Lean 或其他专用形式语言，并在 4.5 小时竞赛时限内完成。
google-deepmind · international-mathematical-olympiad · gemini-deep-think
竞赛 · 证明证据: E2 · 研究记录
H1 · 历史里程碑已有独立佐证
该模型直接处理官方自然语言题目，在评测过程中不使用证明助手或互联网。
openai · openai-experimental-reasoning-model
竞赛 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该管线从 Lean 文件提取定义与定理上下文，让 LLM 提出新的形式命题，再通过 Lean 检查生成结果，并把更困难的候选分离出来供后续训练。论文还报告若干非平凡拓扑学示例，用以说明系统可以产生具有数学用途的命题，而不仅是表面扰动。
auto-res · leanconjecturer · lean · mathlib
系统 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
Mathesis 将非形式题目翻译为 Lean 4 命题，对候选形式化结果的语法与语义质量进行评分，并利用下游证明器反馈偏好能够支撑机器检查证明的命题。Gaokao-Formal 则提供数百道源自中国高考的高难度证明题，用于评测完整管线。
huawei · mathesis · mathesis-autoformalizer · leanscorer · lean
形式化 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
MathArena 在竞赛题目发布后尽快评测模型，并记录模型发布时间与竞赛时间的先后关系。其公开管线既支持最终答案解析，也支持 USAMO、IMO 等证明型竞赛，由专家对模型生成证明进行评分。
eth-zurich · insait · matharena
基准 · 基础设施证据: E3 · 可检查工件
H1 · 历史里程碑论文已发布
该 Agent 维护候选程序种群，使用语言模型提出修改，并通过可执行评估器反复评分。技术报告及结果仓库记录了进化程序在若干数学问题上改进已知构造的案例。
google-deepmind · alphaevolve · gemini
数学发现 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
DeepSeek-V3 先把问题分解为子目标，成功的子目标证明被整理为强化学习的冷启动推理轨迹。
deepseek · deepseek-prover-v2 · lean
证明 · 系统证据: E3 · 可检查工件
H3 · 背景事件论文已发布
R1-Zero 在无 SFT 冷启动的情况下使用强化学习；R1 则加入多阶段训练并开放多个蒸馏模型。
deepseek · deepseek-r1
系统 · 基准证据: E3 · 可检查工件
- 2024
H2 · 领域里程碑论文已发布
该项目把数学常数表示为顶点、公式表示为超边，再搜索能够扩充该关系图的整数关系。配套的 LIReC 软件提供公开数据库与数值关系识别工具，可用于检查和继续扩展这一常数关系库。
ramanujan-machine · technion · ramanujan-library · lirec
数学发现 · 基础设施证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
该基准与六十余位数学家合作构建，强调通常需要专家数小时乃至数天才能解决的问题。
epoch-ai · frontiermath
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
系统在大规模 Lean 数据上执行专家迭代，并使用 critic 选择相对容易的问题、引导更深证明搜索。
shanghai-ai-laboratory · internlm2.5-stepprover · lean
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准在前沿推理模型逐渐接近 MATH 等旧数据集饱和后设计。
shenzhen-research-institute-of-big-data · omni-math
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
LeanAgent 持续接收新的 Lean 仓库，通过 LeanDojo 抽取定理与前提数据，更新动态数据库，渐进训练前提检索器，并搜索带有 `sorry` 的定理证明；成功证明还可回流知识库供后续学习。
caltech · leanagent · lean · leandojo
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准从符号模板生成可控的小学数学题族，在保持底层推理结构的同时改变数值、条件数量与干扰项，从而检验模型成功是否具有稳定性，而非只适用于固定基准实例。
apple · gsm-symbolic · gsm8k
基准 · 数据集证据: E3 · 可检查工件
H3 · 背景事件尚属声明
o1 系列被训练为在给出答案前投入更多推理时计算执行多步思考。
openai · openai-o1
系统 · 基准证据: E1 · 原始声明
H2 · 领域里程碑论文已发布
该模型针对 Lean 4 形式数学进行专门训练，使用 Lean 反馈进行强化学习，并配合带内在奖励的蒙特卡洛树搜索变体探索多样证明路径。DeepSeek 公开了模型权重和复现实验的代码。
deepseek-ai · deepseek-prover-v1-5 · lean
系统 · 证明证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准从真实 Lean 项目和教材中抽取定理，并提供提取新项目上下文的工具。
carnegie-mellon-university · minictx · ntp-toolkit · lean
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
该 workshop 系列从建立之初就以面向数学推理与数学发现的 AI 技术为核心。到第三届时，官方统计已记录数百篇投稿与录用论文、多层级 program committee、论文奖项…
icml
领域建构证据: E2 · 研究记录
H1 · 历史里程碑论文已发布
AlphaProof 在 Lean 中使用强化学习进行形式证明搜索，AlphaGeometry 2 则以更快的神经符号系统处理几何题。2024 年的流程需要专家将题目翻译为形式化表示，并使用最长数日的计算时间。
google-deepmind · international-mathematical-olympiad · alphaproof · alphageometry-2
竞赛 · 证明证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
初始神经与符号证明器只能解决极少数题目，使该集合成为高难度形式推理目标。
university-of-texas-at-austin · putnambench · lean · isabelle · coq
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该方法从已知 tactic 反向生成思考文本，并对新发现且验证通过的证明执行专家迭代。
carnegie-mellon-university · lean-star · lean
证明 · 系统证据: E2 · 研究记录
H2 · 领域里程碑部分核验
获胜系统在 DeepSeekMath-Base 7B 上微调，并结合思维链、Python 工具执行、自一致性与内部验证集。
numina · hugging-face · numinamath
竞赛 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
迭代式生成与过滤管线把自然语言数学问题翻译为 Lean 4 陈述，并进行反向转换。
shanghai-ai-laboratory · lean-workbook · lean
数据集 · 形式化证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
自然语言竞赛题被翻译为 Lean 陈述、过滤、搜索证明，再作为合成训练数据回流。
deepseek · deepseek-prover · lean
证明 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该基准面向前沿文本与多模态模型保持较高难度，并提供细致的评测方法。
tsinghua-university · openbmb · olympiadbench
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
项目把推理、奖励建模、形式任务、数据增强与代码解释器行为统一到序列到序列格式。
shanghai-ai-laboratory · internlm-math
系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该模型在 120B 数学相关 token 上继续预训练，再通过监督与强化学习阶段提升数学推理。
deepseek · deepseekmath
系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
AlphaGeometry 将基于合成定理与证明数据训练的神经语言模型同符号推理引擎结合；语言模型提出辅助构造，符号引擎检查推导。
google-deepmind · new-york-university · alphageometry
证明 · 系统证据: E3 · 可检查工件
- 2023
H1 · 历史里程碑论文已发布
Google DeepMind 将预训练语言模型、评估器与进化式程序搜索结合，让系统搜索可执行程序，而不是直接生成最终数学答案。
google-deepmind · funsearch
数学发现 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该验证器对中间推理步骤评分，而非只判断最终答案，并可用于候选选择或强化学习。
peking-university · deepseek · math-shepherd
系统 · 数据集证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该项目在 Proof-Pile-2 上继续预训练 Code Llama；该语料混合数学网页、科学论文与数学代码。
eleutherai · princeton-university · llemma
系统 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
Agent 在每一步提出战术、在证明助手中执行，将错误或新的目标写回下一轮提示，并维护搜索历史以支持回溯。该架构展示了无需针对任务专门微调，也能把前沿通用模型封装为证明导向 Agent。
university-of-texas-at-austin · copra · gpt-4 · lean · coq
系统 · 形式化证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准把视觉感知与组合式数学推理结合起来。初始研究显示前沿多模态模型与人类表现之间仍有明显差距，公开项目同时提供数据访问、评测代码与模型结果工具。
mathvista
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统通过共享技能库连接 prover 与 evolver：prover 利用检索到的和新生成的引理构造模块化证明，evolver 则对已验证技能进行变换，以提高其通用性、可复用性与复杂度。
lego-prover · isabelle · pisa
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
这些 Agent 学习调用计算库与符号求解器的交互轨迹，而不是仅依赖纯文本思维链。
microsoft-research · tsinghua-university · tora
系统证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
AMS 的这套响应形成于生成式 AI 广泛进入学术活动的第一年。Notices 文章记录，AMS 已在 2023 年 6 月修订 Ethical Guidelines and Journal Policies，采纳 COPE 关于 AI…
american-mathematical-society
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该项目从 Lean 仓库抽取证明状态、战术与前提信息，并提供可编程证明环境。ReProver 在生成战术前检索相关前提，直接处理大规模数学库中的前提选择问题。
caltech · nvidia · leandojo · reprover · lean
基础设施 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统使用类似 AlphaZero 的学习与搜索流程，直接在汇编指令空间中寻找算法。DeepMind 报告短序列最高约 70% 的加速、超长序列约 1.7% 的加速，并公开伪代码、发现的汇编程序及正确性测试。
google-deepmind · alphadev
数学发现 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该项目不只对最终答案给出奖励，而是收集中间推理步骤的人工判断，并据此训练过程奖励模型。PRM800K 公开了研究使用的标注、标注说明以及带评分的模型样本。
openai · process-reward-model · prm800k
系统 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
与逐步预测证明动作并搜索后续路径不同，Baldur 微调语言模型一次生成完整证明；随后由独立的修复模型读取失败证明及证明助手的错误反馈，再提出修正后的证明。
baldur · isabelle-hol
证明 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该基准覆盖分析、线性代数、抽象代数、拓扑等本科教材数学。
yale · carnegie-mellon-university · proofnet · lean
基准 · 数据集证据: E3 · 可检查工件
- 2022
H2 · 领域里程碑论文已发布
语言模型先生成高层形式证明草图，再由自动证明器完成其中的子目标。
meta-ai · university-of-cambridge · draft-sketch-prove
形式化 · 证明证据: E3 · 可检查工件
H1 · 历史里程碑论文已发布
DeepMind 将矩阵乘法表示为张量分解游戏，并训练类似 AlphaZero 的强化学习智能体搜索巨大的分解空间。公开产物包括所发现的分解、基准代码以及算法性质检查工具。
deepmind · alphatensor
数学发现 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
Google Research 在科学论文与数学网页内容上继续预训练大型语言模型，并在数学、物理等定量领域评测逐步推理式解答。该系统直接使用自然语言，而非证明助手。
google-research · minerva
系统 · 基准证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
研究者通过 few-shot prompting 让大语言模型把非形式化数学陈述翻译为 Isabelle/HOL，并将生成的形式化结果进一步作为神经定理证明器的训练数据，把自然语言翻译与形式证明搜索连接到同一流程中。
google-research · university-of-cambridge · isabelle-hol
形式化 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
NaturalProver 在证明生成时让语言模型条件化于定义、定理等数学背景资料，这些资料可以自动检索或由人类提供。
university-of-washington · allen-institute-for-ai · naturalprover · naturalproofs
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
系统从自身证明搜索中继续学习，并使用受蒙特卡洛树搜索与 AlphaZero 启发的超树搜索算法。
meta-ai · htps
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该框架使用定理证明器 hammer 进行前提选择，其余证明决策由语言模型完成。
university-of-cambridge · microsoft-research · thor
证明 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该证明器在不同难度的形式命题上交替执行证明搜索与基于新发现证明的再训练。
openai · lean-statement-curriculum-prover · lean
证明 · 系统证据: E2 · 研究记录
- 2021
H2 · 领域里程碑论文已发布
系统把 clause 编码为图并交由基于 Transformer 的模型评分。训练以增量方式推进，同时使用 hindsight replay 将失败搜索中的中间状态转化为额外学习目标，而不是丢弃这些轨迹。
deepmind · her-theorem-prover
证明 · 系统证据: E2 · 研究记录
H1 · 历史里程碑论文已发布
该项目利用监督式机器学习在大型数学数据集中寻找预测关系，再利用 attribution 方法揭示哪些变量驱动模型预测。数学家随后解释这些信号，将其重新表述为数学命题、寻找反例并给出传统数学论证。
deepmind · university-of-oxford · university-of-sydney · ml-guided-mathematical-discovery
数学发现 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该工作把人工编写的数学推理数据集与生成器—验证器流程结合：语言模型生成多个候选解，另一个单独训练的验证器对候选进行评分并选择最有希望的答案。
openai · gsm8k · learned-verifier
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准把 AIME、AMC、IMO 及教学来源中的问题翻译为形式语言。其贡献不是新的数学定理，而是为学习式定理证明器提供可复现、可训练和可比较的共同目标。
openai · formal-mathematics-community · minif2f · lean · metamath · isabelle · hol-light
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
MATH-AI 最初以跨学科 workshop 形式讨论数学推理如何帮助理解一般人工智能。首届议程结合邀请报告、投稿论文、poster session 与讨论 panel，并采用匿名投稿评审。
iclr · neurips
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该基准覆盖代数、几何、数论、概率等竞赛数学主题，并提供完整解题过程。
uc-berkeley · math-benchmark
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统把证明搜索整体表述为端到端强化学习问题，并引入回溯机制，使智能体能够放弃预测为死路的推导并从更有希望的分支继续搜索。最终证明在 HOL4 内构造，因此仍接受证明助手内核检查。
australian-national-university · csiro-data61 · tacticzero · hol4
证明 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该方法从内核级证明项中提取自监督目标，并与 tactic prediction 一起训练。
openai · pact · lean
证明 · 系统证据: E3 · 可检查工件
- 2020
H2 · 领域里程碑论文已发布
OpenAI 研究者 Stanislas Polu 与 Ilya Sutskever 在形式数学文本上训练生成模型，并将其整合进 Metamath 的证明搜索。
openai · metamath-community · gpt-f · metamath
证明 · 形式化证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该项目把在线 tactic 学习、证明搜索与 package-aware instrumentation 结合起来，使机器学习辅助直接存在于证明助手工作流中，而不是停留在独立的 benchmark 实验里。
tactician · coq
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该基准从公理出发生成合成不等式证明，并系统改变训练与测试分布的属性，使研究者能够区分近似记忆式成功与不同形式的分布外定理证明泛化。
university-of-toronto · vector-institute · int-benchmark
基准 · 基础设施证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
IsarStep 将声明式 Isar 证明转换为序列到序列样本，并移除其中的中间命题。任务要求模型重建连接前后证明状态的语义桥梁；作者评测了 Transformer 类基线，并设计面向长证明上下文的分层架构。
university-of-cambridge · isarstep · isabelle
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
Skip-tree 不只遮蔽扁平 token 序列，而是从结构化数学表达式中移除一个子树并要求模型重建，从而促使表示学习利用形式数学的组合结构。
google-research · skip-tree
系统 · 基础设施证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
该工作把数学语篇理解明确表述为检索问题，而不仅是答案生成问题。其数据集记录 ProofWiki 中 conjecture、定义与支持命题之间的关系，并通过基线方法及后续图模型实验衡量模型恢复证明相关参考资料的能力。
university-of-manchester · nl-ps · ps-proofwiki
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统从既有形式数学中学习，生成额外的定理—证明对，再把合成语料反馈到证明器训练中，而不是仅依赖稀缺的人工证明轨迹。
princeton-university · metagen · metamath
证明 · 系统证据: E3 · 可检查工件
- 2019
H2 · 领域里程碑论文已发布
CoqGym 从开源 Coq 项目中抽取证明状态、环境、目标、tactics 与证明树，并通过可编程交互层暴露这些信息。
princeton-university · coqgym · astactic · coq
系统 · 基准证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
HOList 对 HOL Light 进行工程化封装，使学习系统能够通过机器学习环境与证明状态和 tactics 交互。
google-research · holist · deephol · hol-light
系统 · 基准证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
原始版本为每个模块提供数百万规模的生成式问答样本，并在常规测试划分与外推设置上评估当时的序列到序列神经网络。配套开源生成器使研究者能够复现并扩展任务分布，而不仅依赖固定的静态题目列表。
deepmind · mathematics-dataset
基准 · 数据集证据: E3 · 可检查工件
- 2018
H2 · 领域里程碑论文已发布
GamePad 对 Coq 进行工程化封装，使证明状态、证明步骤、中层与内核级项以及证明树都能表示为 Python 数据结构。
university-of-california-berkeley · openai · gamepad · coq
系统 · 基础设施证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统反复执行证明搜索模拟，把成功与失败的尝试转化为学习信号，并重新训练后续搜索所使用的引导策略。方法在大型形式数学问题语料上进行评测，重点是学习式搜索控制，而非针对具体定理手写启发式规则。
university-of-innsbruck · rl-theorem-prover
系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
作者通过将 Mizar 陈述 informalize 为类似 LaTeX 的数学文本，构建大规模对齐语料，并训练序列到序列翻译模型重建形式语言。研究比较多种神经翻译配置，并通过案例分析模型能够正确恢复哪些数学结构。
university-of-innsbruck · mizar
形式化证据: E2 · 研究记录
- 2017
H2 · 领域里程碑尚属声明
Mathlib 将社群编写的 Lean 定义、定理、证明与 tactics 组织为共享数学库，逐步覆盖代数、分析、拓扑、数论等领域；统一 API 与协作审查实践使形式化成果能够相互复用，而非停留在彼此隔离的项目中。
leanprover-community · lean · mathlib3
形式化 · 基础设施证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
TacticToe 从 HOL4 中记录 tactic 级证明信息，学习在新目标状态下哪些证明动作更有希望，并直接在高阶逻辑环境中搜索完整 tactic 序列，而不是把每个问题都翻译到一阶逻辑。
tactictoe · hol4
系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
HolStep 从 HOL Light 证明中抽取中间陈述与 conjecture，对文本表示进行规范化，并把实际使用的证明步骤与负样本配对。
university-of-innsbruck · google-research · holstep · hol-light
基准 · 数据集证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
该系统从成功自动证明的 clause-level 轨迹中学习，并在 saturation-style proof search 中对生成的 clauses 进行排序。
google-research · university-of-innsbruck · e-prover · deep-network-guided-proof-search
系统证据: E2 · 研究记录
- 2016
H2 · 领域里程碑论文已发布
该系统从对齐语料中学习如何解析有歧义的数学记号，再使用形式语义约束排除语法上合理但类型不成立或缺乏支持的解释。由此形成统计学习与符号推理结合的混合流程：学习模型提出形式结构，类型检查和定理证明机制帮助筛选与验证候选。
university-of-innsbruck · czech-technical-university · semantic-parsing-math · hol-light
形式化证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
Holophrasm 将 Metamath 陈述解析为树结构，训练用于证明步骤生成与证明状态评估的神经模型，并与候选证明树搜索结合。
holophrasm · metamath
证明 · 系统证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
DeepMath 使用循环与卷积神经架构编码猜想和候选前提，并学习判断某个前提是否有助于目标定理。该工作把大型形式证明语料转化为神经相关性模型的训练数据，使表示学习成为自动定理证明流程中的核心组件之一。
google-research · czech-technical-university · deepmath · mizar
系统证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
AITP 2016 明确将自身定位为讨论如何把 AI 与推理方法用于大规模数学和科学语料的论坛。首届议程设置了面向 ATP / ITP 与数学的 AI、非形式与半形式数学理解、现代 AI 方法等专题，并包含投稿报告。
university-of-innsbruck
领域建构证据: E2 · 研究记录
- 2015
H2 · 领域里程碑尚属声明
项目聚焦大型复杂理论、从推理轨迹学习、演绎与学习之间的反馈循环，以及跨多种数学表示风格积累推理知识。
czech-technical-university · european-research-council
领域建构证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
Lean 在一个开放平台中结合小型证明检查内核、富表达力的依赖类型理论、交互式证明开发与可扩展自动化，并同时面向形式化数学与验证任务。
microsoft-research · carnegie-mellon-university · lean
系统 · 基础设施证据: E3 · 可检查工件
- 2014
H2 · 领域里程碑论文已发布
完成后的工程同时形式化克卜勒猜想证明的数学文本与大型计算部分。
flyspeck · hol-light · isabelle
形式化 · 证明证据: E3 · 可检查工件
- 2013
H2 · 领域里程碑论文已发布
系统把快速学习式相关性方法扩展到约 15 万条 MML 公式，并部署到 MizAR 在线推理服务。
university-of-innsbruck · mizar · mizar40 · mizar-online-reasoning
系统 · 基准证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
用户可以上传 HOL Light 工程，并让服务使用学习式相关性模型、并行 ATP 组合与决策过程处理新猜想。
university-of-innsbruck · holyhammer · hol-light
系统 · 基础设施证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
项目在形式化定理本身的同时，建立了覆盖群论、线性代数、Galois 理论及实/复代数数的大规模数学库。
microsoft-research · inria · coq
形式化 · 证明证据: E2 · 研究记录
- 2010
H2 · 领域里程碑论文已发布
Sledgehammer 自动选择 Isabelle 相关事实，将证明义务翻译给外部 ATP，并利用返回结果帮助构造由证明助手检查的证明。
university-of-cambridge · sledgehammer · isabelle
系统 · 基础设施证据: E2 · 研究记录
- 2007
H2 · 领域里程碑尚属声明
竞赛提供统一的 Mizar 衍生问题、公开规则与总资源预算，使学习、前提选择和其他大型理论推理策略能够直接比较。
mptp
竞赛 · 基准证据: E3 · 可检查工件
H2 · 领域里程碑论文已发布
系统反复从已有证明训练相关性模型，在筛选前提上调用自动证明器，并把新找到的证明纳入后续学习轮次。
charles-university · malarea
系统证据: E2 · 研究记录
- 2005
H2 · 领域里程碑论文已发布
该形式化把组合论证与计算机分类检查都纳入 Coq，使正确性依赖通用证明助手验证机制，而非四色定理专用外部程序。
microsoft-research · coq
形式化 · 证明证据: E2 · 研究记录
- 2003
H2 · 领域里程碑尚属声明
项目计划同时形式化 Hales 证明中的书面数学论证与计算机计算部分，最终主要使用 HOL Light 与 Isabelle 完成。
flyspeck · hol-light · isabelle
形式化 · 基础设施证据: E2 · 研究记录
- 1998
H2 · 领域里程碑论文已发布
HR 搜索数学概念空间、评估概念的有趣程度，并利用生成概念继续驱动例子、分类与猜想探索。
university-of-edinburgh · hr
数学发现 · 系统证据: E2 · 研究记录
- 1996
H2 · 领域里程碑论文已发布
自动搜索在一个数十年未解决、长期接受人类与机器尝试的问题上产生了紧凑的等式推导。
argonne-national-laboratory · eqp · otter
证明 · 数学发现证据: E3 · 可检查工件
H2 · 领域里程碑尚属声明
各系统在共享计算环境与标准化定理证明问题上评测，使性能比较更可复现、更透明。
cade · casc
竞赛 · 基准证据: E2 · 研究记录
- 1994
H2 · 领域里程碑论文已发布
QED 是领域建构愿景而非单一软件发布，主张围绕共享形式数学知识开展广泛协作。
领域建构证据: E2 · 研究记录
- 1993
H2 · 领域里程碑尚属声明
TPTP 以统一格式整理 ATP 测试问题，并建立领域分类与版本发布规范，使定理证明器能够在可比较输入上进行测试。
tptp
基准 · 数据集证据: E3 · 可检查工件
- 1992
H2 · 领域里程碑尚属声明
Metamath 将极小验证器与显式证明对象分离，使大型形式数学语料可以由最小可信机制进行检查。
metamath
形式化 · 基础设施证据: E3 · 可检查工件
- 1988
H2 · 领域里程碑论文已发布
Isabelle 利用高阶合一与通用元逻辑架构编码多种对象逻辑，并通过 tactics 与 tacticals 提供自动化。
university-of-cambridge · isabelle
形式化 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
HOL 结合小型可信逻辑基础、ML 编程与 tactics/tacticals，在高阶逻辑中支持目标驱动的交互式证明。
university-of-cambridge · hol · lcf
形式化 · 系统证据: E2 · 研究记录
- 1986
H2 · 领域里程碑论文已发布
Nuprl 将构造类型论、refinement 式证明开发、tactics 与证明的计算解释结合起来；完整证明可以用于提取满足形式规格的程序，从而在同一环境中连接定理证明、形式数学与 verified programming。
cornell-university · nuprl
形式化 · 系统证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
Graffiti 评估图不变量之间的候选关系，保留在已知图中没有反例的陈述，并用启发式删除平凡或重复猜想。
university-of-houston · graffiti
数学发现 · 系统证据: E2 · 研究记录
- 1984
H2 · 领域里程碑尚属声明
该系统为 Calculus of Constructions 中的证明提供机器检查，并经过持续演化成为 Coq，后更名为 Rocq。
inria · coq · calculus-of-constructions
形式化 · 系统证据: E2 · 研究记录
- 1979
H2 · 领域里程碑论文已发布
Edinburgh LCF 不再依赖保存完整证明对象，而是通过受限的抽象接口产生 theorem 值，其构造操作对应公理与推理规则。
university-of-edinburgh · edinburgh-lcf · lcf
形式化 · 系统证据: E2 · 研究记录
- 1977
H2 · 领域里程碑论文已发布
AM 维护潜在有趣数学任务的 agenda，并利用通用启发式决定下一步探索哪些概念、例子与猜想。
stanford-ai-lab · am
数学发现 · 系统证据: E2 · 研究记录
H2 · 领域里程碑尚属声明
该方法把初等几何代数化：将几何构型编码为多项式方程，并把定理证明转化为符号多项式推理。吴文俊在 Ritt 特征列思想与构造性消元基础上发展出机械化证明路线，并能显式处理退化情形。
chinese-academy-of-sciences
证明 · 基础设施证据: E2 · 研究记录
- 1973
H2 · 领域里程碑尚属声明
Mizar 发展形式数学语言、检查器与数学库模式，目标是形成可累积的计算机可验证数学体系。
mizar
形式化 · 基础设施证据: E2 · 研究记录
H2 · 领域里程碑论文已发布
PLTP 面向基于归结的一阶证明器难以处理的递归程序性质，采用以化简与归纳为核心的专门证明过程。
university-of-edinburgh · pltp
证明 · 系统证据: E3 · 可检查工件
- 1972
H2 · 领域里程碑论文已发布
Stanford LCF 允许用户提出证明目标、分解子目标，并通过化简与推理命令构造由机器检查的形式推导。它早于 Edinburgh LCF 中可扩展的 ML 元语言、抽象 theorem 类型与可编程 tactics。
stanford-university · stanford-lcf · lcf
形式化 · 基础设施证据: E2 · 研究记录
- 1971
H2 · 领域里程碑论文已发布
MACSYMA 在可交互、可扩展系统中整合有理函数、代数化简、微积分及相关符号运算。
mit-project-mac · macsyma
系统 · 基础设施证据: E2 · 研究记录
- 1968
H2 · 领域里程碑论文已发布
Automath 以高度显式的有类型形式语言表示定义、命题与证明，使计算机能够检查推导的正确性。
eindhoven-university-of-technology · automath
形式化 · 基础设施证据: E2 · 研究记录
- 1965
H2 · 领域里程碑论文已发布
该方法通过合一处理代换，并使用统一的归结推理模式，取代早期机器定理证明中效率较低的交替过程。
argonne-national-laboratory
基础设施证据: E2 · 研究记录
- 1961
H2 · 领域里程碑论文已发布
SAINT 将积分表示为搜索问题，利用经验规则选择变换与代换，把积分逐步化为可求解形式。
mit-lincoln-laboratory · saint
系统证据: E2 · 研究记录
- 1960
H2 · 领域里程碑论文已发布
系统把符号演绎与几何信息结合，用于剪除不合理的证明路径，展示了早期的领域知识驱动启发式推理。
ibm-research · geometry-theorem-machine
证明 · 系统证据: E2 · 研究记录
- 1956
H2 · 领域里程碑论文已发布
系统编码逻辑表达式并搜索允许的变换空间，利用启发式优先探索更有希望的分支，而非完全穷举。
rand-corporation · carnegie-tech · logic-theorist
证明 · 系统证据: E2 · 研究记录
- 1955
H3 · 背景事件论文已发布
该提案并未建立独立的 AI4Math 领域，但确立了更广义的 AI 研究框架，而数学推理很快成为检验机器智能的早期核心场景之一。
dartmouth-college
领域建构证据: E2 · 研究记录
没有匹配的时间线事件当前搜索、事件类型或重要性条件没有匹配结果。可以调整条件，或一键恢复完整时间线。
恢复完整时间线 