搜索、组合条件并比较事件

公开仓库包含总览、手稿索引、PDF 与源码、Lean 库与形式化目录、十个精选 reasoning summaries，以及保存公开版本历史的承诺。OpenAI 明确提醒部分未形式化结果可能存在问题， 并表示后续修订将保留历史版本。此次发布此前与独立的 Advisory Group on Mathematics and Artificial Intelligence 进行了沟通；AGMAI 随后公开声明，其建议不构成对数学结果 或 OpenAI 流程的背书，并把本次发布视为更广泛人类理解与共同体评估的开始。

论文的方法部分说明，Anthropic 员工最初让内部研究模型研究一个基于 average-case Zero-k-Clique 的密码学问题。Claude 在约 1,600 万 output tokens、无人类输入的 session 中意外发展出新算法，先处理平均情形，再推广到最坏情形。Anthropic 将结果 提供给 Alman 与 Vassilevska Williams；两位作者随后重新理解论证、简化方法、 改进常数与指数、推出更多后果并撰写论文。论文完成后，Anthropic 又使用研究模型 把主要 deterministic claims 形式化到 Lean 中。

作者在致谢中明确表示，论文中的大多数证明与数学思想由 ChatGPT 找到；其中 suspension idea 被特别指出为人类作者提出的重要贡献。作者把自己的主要作用描述为理解模型给出的 证明、检查和组织数学内容并改善阐释。目前该成果仍是一篇非常新的预印本；Chronicle 尚未找到公开 proof-assistant artifact 或足以把事件提升到更高验证状态的独立专业审查。

Meta 表示，人类数学家负责选题并引导研究，另有一组数学家对工作进行审查；每篇论文标记 哪些段落主要由研究者或 AI 起草，并明确引用已有及同期工作。Muse Spark 在不同项目中的 作用并不相同：它协助测试与修订计算，生成 GAP 搜索程序并找到一个 384 阶群反例， 提出反例与证明策略，还生成候选证明并起草技术章节。Meta 同时承认若干问题被其他团队 独立解决，其中包括 Nilradical AI agent 在 Meta 发布前报告的另一 semiabelian-group 反例。

AGMAI 表示该建议吸收了数学共同体超过 600 份反馈。文件区分两类情形：由负责的数学家 完整理解的普通论文，以及尚无人类完整理解的 AI 输出。针对后一类，文件既提出技术发布 规范，也要求实验室为独立、共同体主导的研讨会、会议、阐释工作及其他理解和吸收数学 所需活动提供支持；同时警告前沿系统访问不平等可能制造多层级的数学共同体。

FrenzyMath 报告该项目约包含 320 万行 Lean，LLM 与计算服务器总成本低于 3 万美元。 仓库将仅依赖 Mathlib 的 endpoint statements 与证明库分离，并保存 Comparator 配置、 verifier 版本、日志和源码 provenance 记录。公告同时指出，Ziyang Qin、Yuan Liao、 Ayush Khaitan 与 Bennett Chow 等组成的独立团队在同一天稍早也发布了另一套完整 庞加莱 Lean 开发；该独立 arXiv 论文记录了公开全量构建，并说明证明与文字工作中使用了 自动化辅助。

该组织说明，其形成始于 OpenAI 接触部分后来的成员，希望建立外部顾问委员会； 在与 OpenAI 沟通后，这些数学家决定改为成立一个独立组织并邀请其他成员加入。 首批成员包括 François Charles、Camillo De Lellis、Timothy Gowers、Martin Hairer、 Nikhil Srivastava、Ulrike Tillmann、Ravi Vakil、Edward Witten 与 Melanie Matchett Wood。该组织当前明确的首项任务，是就 OpenAI 所称由内部模型 产生的大量重要数学成果如何协调发布向其提供建议。OpenAI 的公告同时明确引用 《A Severe Misalignment of AI in Mathematics》，将其列为建立这一数学共同体 沟通渠道的直接背景之一。

该档案库有意采用不同于 Mathlib 的定位：它接收可能不适合 Mathlib 高度整合式库结构 的独立完整形式化项目，同时施加自动化维护与质量检查。公开仓库说明，目前项目导入 仍由人类选择，而 AI 系统实质参与审查、维护与优化。由于库规模持续变化，本 Event 不把某一时点的项目数或代码行数作为冻结的历史主张。

FormalFlow 以共享 blueprint 为核心，将长程形式化组织为嵌套的规划、证明与审查循环。 AI Agent 负责实现和审查证明任务，人类则监督整体项目、对照形式化开发与原始数学文本， 并处理语义偏差。公开的 MIPStarRE 仓库保存 Lean 源码、活动 blueprint、源论文材料 以及面向 CI 的证明完整性基础设施。

公开项目提供一篇未署名数学论文、基于 mathlib Liouville 函数的完整 Lean 4 形式化、固定工具链元数据、构建与公理审计以及证明路线检查。另一个独立审计仓库 在 Linux 上重新构建冻结的 v1.0.0 产物，对照源码哈希并重复公理与路线审计， 报告未发现 sorry、自定义定理公理或 native_decide。由于公开论文和仓库没有保存 详细的模型—人类推导轨迹，Chronicle 对具体智力分工只做来源归因，不作独立重建。

该声明形成于一周内围绕 AI 数学能力快速提升和高关注度数学问题求解展开的密集讨论。其核心框架是：企业以 benchmark 和竞赛式突破为导向的激励，可能与数学共同体重视理解、交流、归属、人才培养和长期知识积累的价值发生错位。9 月 14 日，IMPA 在机构新闻页面转载声明；9 月 15 日，法国数学会理事会在回应 OpenAI Navier–Stokes 公告及相关伦理争议的正式立场中直接引用该声明。

Magenta 使用 statement judge 检查生成的 Lean 命题是否保持原始非形式问题的含义，并使用 error-attribution judge 判断失败尝试应回到数学推导还是进行局部 Lean 修复。论文报告称，这种基于反馈的纠错闭环在困难问题上优于独立重采样。

两位研究者明确将底层强迫爆破研究路线归功于 Diego Córdoba 与 Luis Martínez-Zoroa，并描述其使用 LLM 将该路线从较粗糙的外力条件推进到光滑外力及相关流体方程。公开的 `fluid_lean` 仓库包含 Euler 与 Boussinesq 定理的完整 Lean 开发，其文档将 Lean 代码归因于在 Alpöge 指导下工作的 Claude。

OpenAI 表示成功搜索约使用 10,000 个并发 Agent 工作约 88 小时，随后继续进行 Lean 形式化与验证。独立报道确认了这一发布事件，同时也记录了围绕 Tristan Buckmaster 与 Levent Alpöge 同期工作的归属、来源与优先权争议。OpenAI 现表示，经调查确认，Buckmaster 在 9 月 8 日发布前两个月内提交给 Codex 的 prompts 不可能以任何方式影响该系统，包括通过训练产生影响。这一直接声明缩小了 provenance 争议中的一个子问题，但围绕归属、优先权和合作过程的其他争议仍然存在于公开记录中。

该基准覆盖马尔可夫链、更新过程、随机游走、鞅、停时、排队论、布朗运动、随机微积分、弱收敛、泊松过程与连续时间马尔可夫过程。公开数据集区分 114 个直接形式化目标与 336 个抽象化目标：当固定 Lean / Mathlib 环境缺少所需随机过程基础设施时，后者会把必要性质显式写入假设。

Claude Agent 使用 Anthropic 的 Prove2Me 工作流构建形式化子问题依赖图，并将其扩展为数百万行 Lean 代码。仓库沿用经典的 Frey–Serre–Ribet–Wiles–Taylor-Wiles 路线，并公开定理依赖图、来源归属和可复现验证流程。

公开的 PrimeGaps186 仓库包含 DHL[40,2] 与 186 素数间隔结论的 Lean 4 开发， 并附带 Python/FLINT 数值 certificate。登记的主要 Lean declaration 均无 sorry， OpenAI 报告 Comparator、Nanoda 与 Lean kernel 均接受这些条件式证明。但形式化 仍依赖三个显式项目公理：一个 rank-three hyper-Kloosterman 估计、一个 rank-two Kloosterman correlation 估计，以及一组 physical-integral 与 cap bounds。前两个 输入来自既有文献；数值输入由配套 certificate 检查，而没有在 Lean 内证明。 OpenAI 自身的 metadata 将审查状态标为 self-assessed，并明确说明尚无独立人类 semantic review。

Palomar 的设立背景是 machine-assisted / machine-generated mathematics 数量快速增加， 而成果分散在代码仓库和公告中，外部读者难以核查。其公开声明把该服务定位为形式化成果 的 preprint / repository 层：提供不可变、可搜索、可检查的机械验证记录，同时把新颖性、 相关性和更深层数学判断留给研究共同体。

Claude 协调数十个子 Agent、检索文献并进行数值检查，随后生成论文；Anthropic 数学家审核结果，Lean 形式化通过 comparator。

OpenAI 表示内部 Astra 模型生成数学论证，人类与模型共同整理稿件，随后模型把每项论证形式化为 Lean certificate。后续报道记录了围绕非 sofic 群结果的归属与训练数据来源争议，其中包括 Andreas Thom 尚未得到解决的问题：他与同事通过 ChatGPT 进行的未公开数学讨论，是否可能通过模型改进数据间接影响相关系统。

问题由数学家筛选，并尽可能配套专用计算验证器，同时按解答的重要性进行分级。

该试点仅允许使用中间检查点、训练协议和训练数据均公开的模型。6 支团队在 6 道证明题上产出有效提交；AIMO 使用同一专家评分流程，将这些结果与开放权重及商业前沿模型比较，并公开提交内容与详细评分数据。

该声明源于 2025 年 9 月 Lorentz Center 举办的一次会议，约 60 名参与者来自 10 个国家，背景覆盖数学、计算机科学、哲学、历史、社会科学、产业与政府。随后较小的工作组在数月内结合广泛共同体反馈形成文本。声明以 DOI 形式存档于 Zenodo，获得 IMU endorsement，之后在 ICM 2026 公开讨论，并受到主要科学出版物的社论与报道关注。

AlphaProof Nexus 让前沿 LLM 子 Agent 围绕 Lean 编译器工作，并通过专用工具与进化搜索逐级增强证明搜索。项目公开了成功解决的 Erdős、OEIS 与科研协作案例的 Lean 证明，并为部分结果提供人类可读证明说明。

模型使用代数数论工具发现构造；OpenAI 同时发布证明与由外部数学家撰写的 companion paper，后者检查并解释了论证。

SorryDB 抓取符合条件的公开 Lean 仓库，为尚未完成的 `sorry` 命题记录可复现的仓库与工具链坐标，并要求证明系统在原始项目上下文中填补证明缺口。验证器会重建相应项目并检查候选证明，夜间更新的数据库则持续提供新任务。

内部模型在有限人工监督下工作；研究者有时要求重试或澄清，并在人类判断下选择候选尝试。

M2F 首先把长篇数学文档翻译为按依赖排序的 Lean 声明骨架，并修复项目层面的结构不一致；随后固定命题签名，利用验证器反馈迭代填补证明缺口。配套 ReasBook 仓库公开了由教材和研究论文生成的形式化项目。

Aletheia 将高级 Gemini Deep Think 模型与迭代验证、修订及密集工具使用结合，面向需要文献导航和长证明链的研究环境。作者还明确区分不同自主性与新颖性层级，而非把所有 AI 辅助结果视为同一种贡献。

该系统以通用 Coding Agent 循环作为 Lean 工作的控制器，并通过面向 MCP 的接口接入定理检索、非形式证明、验证和辅助推理工具。公开仓库提供安装说明、可运行的 Agent 工具以及 Putnam 形式证明产物。

该论文研究最大似然估计在数据增加时其期望预测误差是否单调改善，证明若干 Gaussian 与 Gamma 情形下的 forward-KL 单调性，并给出适用于广泛指数族的 reverse-KL 论证。OpenAI 将其作为 GPT-5.2 Pro 直接参与此前未解决数学问题的案例公开介绍。

GPT-5 提出多个方向和若干关键结构性想法；Ryu 负责检查与重构，并与 Uijeong Jang 写成严格的最终证明。

该架构生成并形式化有用引理、搜索形式证明，并通过专用组件处理几何。

系统采用脚手架式数据合成、验证器引导的迭代修复与模型平均。

系统依据 Lean 反馈迭代改进整段证明，并使用深度与广度相结合的测试时搜索策略。

与 2024 年的 AlphaProof 和 AlphaGeometry 2 不同，2025 年系统直接读取官方题目并生成自然语言证明，无需人工翻译成 Lean 或其他专用形式语言，并在 4.5 小时竞赛时限内完成。

该模型直接处理官方自然语言题目，在评测过程中不使用证明助手或互联网。

该管线从 Lean 文件提取定义与定理上下文，让 LLM 提出新的形式命题，再通过 Lean 检查生成结果，并把更困难的候选分离出来供后续训练。论文还报告若干非平凡拓扑学示例，用以说明系统可以产生具有数学用途的命题，而不仅是表面扰动。

Mathesis 将非形式题目翻译为 Lean 4 命题，对候选形式化结果的语法与语义质量进行评分，并利用下游证明器反馈偏好能够支撑机器检查证明的命题。Gaokao-Formal 则提供数百道源自中国高考的高难度证明题，用于评测完整管线。

MathArena 在竞赛题目发布后尽快评测模型，并记录模型发布时间与竞赛时间的先后关系。其公开管线既支持最终答案解析，也支持 USAMO、IMO 等证明型竞赛，由专家对模型生成证明进行评分。

该 Agent 维护候选程序种群，使用语言模型提出修改，并通过可执行评估器反复评分。技术报告及结果仓库记录了进化程序在若干数学问题上改进已知构造的案例。

DeepSeek-V3 先把问题分解为子目标，成功的子目标证明被整理为强化学习的冷启动推理轨迹。

R1-Zero 在无 SFT 冷启动的情况下使用强化学习；R1 则加入多阶段训练并开放多个蒸馏模型。

该项目把数学常数表示为顶点、公式表示为超边，再搜索能够扩充该关系图的整数关系。配套的 LIReC 软件提供公开数据库与数值关系识别工具，可用于检查和继续扩展这一常数关系库。

该基准与六十余位数学家合作构建，强调通常需要专家数小时乃至数天才能解决的问题。

系统在大规模 Lean 数据上执行专家迭代，并使用 critic 选择相对容易的问题、引导更深证明搜索。

该基准在前沿推理模型逐渐接近 MATH 等旧数据集饱和后设计。

LeanAgent 持续接收新的 Lean 仓库，通过 LeanDojo 抽取定理与前提数据，更新动态数据库，渐进训练前提检索器，并搜索带有 `sorry` 的定理证明；成功证明还可回流知识库供后续学习。

该基准从符号模板生成可控的小学数学题族，在保持底层推理结构的同时改变数值、条件数量与干扰项，从而检验模型成功是否具有稳定性，而非只适用于固定基准实例。

o1 系列被训练为在给出答案前投入更多推理时计算执行多步思考。

该模型针对 Lean 4 形式数学进行专门训练，使用 Lean 反馈进行强化学习，并配合带内在奖励的蒙特卡洛树搜索变体探索多样证明路径。DeepSeek 公开了模型权重和复现实验的代码。

该基准从真实 Lean 项目和教材中抽取定理，并提供提取新项目上下文的工具。

该 workshop 系列从建立之初就以面向数学推理与数学发现的 AI 技术为核心。到第三届时，官方统计已记录数百篇投稿与录用论文、多层级 program committee、论文奖项，以及覆盖自动形式化语义对齐、理论计算机科学证明、视觉科学推理与端到端 Lean 证明生成的四个 challenge track。

AlphaProof 在 Lean 中使用强化学习进行形式证明搜索，AlphaGeometry 2 则以更快的神经符号系统处理几何题。2024 年的流程需要专家将题目翻译为形式化表示，并使用最长数日的计算时间。

初始神经与符号证明器只能解决极少数题目，使该集合成为高难度形式推理目标。

该方法从已知 tactic 反向生成思考文本，并对新发现且验证通过的证明执行专家迭代。

获胜系统在 DeepSeekMath-Base 7B 上微调，并结合思维链、Python 工具执行、自一致性与内部验证集。

迭代式生成与过滤管线把自然语言数学问题翻译为 Lean 4 陈述，并进行反向转换。

自然语言竞赛题被翻译为 Lean 陈述、过滤、搜索证明，再作为合成训练数据回流。

该基准面向前沿文本与多模态模型保持较高难度，并提供细致的评测方法。

项目把推理、奖励建模、形式任务、数据增强与代码解释器行为统一到序列到序列格式。

该模型在 120B 数学相关 token 上继续预训练，再通过监督与强化学习阶段提升数学推理。

AlphaGeometry 将基于合成定理与证明数据训练的神经语言模型同符号推理引擎结合；语言模型提出辅助构造，符号引擎检查推导。

Google DeepMind 将预训练语言模型、评估器与进化式程序搜索结合，让系统搜索可执行程序，而不是直接生成最终数学答案。

该验证器对中间推理步骤评分，而非只判断最终答案，并可用于候选选择或强化学习。

该项目在 Proof-Pile-2 上继续预训练 Code Llama；该语料混合数学网页、科学论文与数学代码。

Agent 在每一步提出战术、在证明助手中执行，将错误或新的目标写回下一轮提示，并维护搜索历史以支持回溯。该架构展示了无需针对任务专门微调，也能把前沿通用模型封装为证明导向 Agent。

该基准把视觉感知与组合式数学推理结合起来。初始研究显示前沿多模态模型与人类表现之间仍有明显差距，公开项目同时提供数据访问、评测代码与模型结果工具。

该系统通过共享技能库连接 prover 与 evolver：prover 利用检索到的和新生成的引理构造模块化证明，evolver 则对已验证技能进行变换，以提高其通用性、可复用性与复杂度。

这些 Agent 学习调用计算库与符号求解器的交互轨迹，而不是仅依赖纯文本思维链。

AMS 的这套响应形成于生成式 AI 广泛进入学术活动的第一年。Notices 文章记录，AMS 已在 2023 年 6 月修订 Ethical Guidelines and Journal Policies，采纳 COPE 关于 AI 工具不能作为作者、AI 使用必须披露的立场。7 月建立的咨询组则把响应从即时 journal rules 扩展为对数学研究与职业共同体的持续治理议题；其 2024 年 white papers 被明确设计为供 AMS 政策委员会与更广泛共同体持续更新使用的资源。

该项目从 Lean 仓库抽取证明状态、战术与前提信息，并提供可编程证明环境。ReProver 在生成战术前检索相关前提，直接处理大规模数学库中的前提选择问题。

该系统使用类似 AlphaZero 的学习与搜索流程，直接在汇编指令空间中寻找算法。DeepMind 报告短序列最高约 70% 的加速、超长序列约 1.7% 的加速，并公开伪代码、发现的汇编程序及正确性测试。

该项目不只对最终答案给出奖励，而是收集中间推理步骤的人工判断，并据此训练过程奖励模型。PRM800K 公开了研究使用的标注、标注说明以及带评分的模型样本。

与逐步预测证明动作并搜索后续路径不同，Baldur 微调语言模型一次生成完整证明；随后由独立的修复模型读取失败证明及证明助手的错误反馈，再提出修正后的证明。

该基准覆盖分析、线性代数、抽象代数、拓扑等本科教材数学。

语言模型先生成高层形式证明草图，再由自动证明器完成其中的子目标。

DeepMind 将矩阵乘法表示为张量分解游戏，并训练类似 AlphaZero 的强化学习智能体搜索巨大的分解空间。公开产物包括所发现的分解、基准代码以及算法性质检查工具。

Google Research 在科学论文与数学网页内容上继续预训练大型语言模型，并在数学、物理等定量领域评测逐步推理式解答。该系统直接使用自然语言，而非证明助手。

研究者通过 few-shot prompting 让大语言模型把非形式化数学陈述翻译为 Isabelle/HOL，并将生成的形式化结果进一步作为神经定理证明器的训练数据，把自然语言翻译与形式证明搜索连接到同一流程中。

NaturalProver 在证明生成时让语言模型条件化于定义、定理等数学背景资料，这些资料可以自动检索或由人类提供。项目同时研究下一步证明建议与完整证明生成，并公开 NaturalProofs-Gen 数据、训练与生成代码、评测工具和模型资源。

系统从自身证明搜索中继续学习，并使用受蒙特卡洛树搜索与 AlphaZero 启发的超树搜索算法。

该框架使用定理证明器 hammer 进行前提选择，其余证明决策由语言模型完成。

该证明器在不同难度的形式命题上交替执行证明搜索与基于新发现证明的再训练。

系统把 clause 编码为图并交由基于 Transformer 的模型评分。训练以增量方式推进，同时使用 hindsight replay 将失败搜索中的中间状态转化为额外学习目标，而不是丢弃这些轨迹。

该项目利用监督式机器学习在大型数学数据集中寻找预测关系，再利用 attribution 方法揭示哪些变量驱动模型预测。数学家随后解释这些信号，将其重新表述为数学命题、寻找反例并给出传统数学论证。Nature 论文以双曲纽结和 Kazhdan-Lusztig 多项式为两个案例展示这一流程，并公开了相应 notebook 与数据。

该工作把人工编写的数学推理数据集与生成器—验证器流程结合：语言模型生成多个候选解，另一个单独训练的验证器对候选进行评分并选择最有希望的答案。

该基准把 AIME、AMC、IMO 及教学来源中的问题翻译为形式语言。其贡献不是新的数学定理，而是为学习式定理证明器提供可复现、可训练和可比较的共同目标。

MATH-AI 最初以跨学科 workshop 形式讨论数学推理如何帮助理解一般人工智能。首届议程结合邀请报告、投稿论文、poster session 与讨论 panel，并采用匿名投稿评审。随着领域演化，后续各届逐步覆盖大语言模型、定理证明、自动形式化、数学发现与 Agentic AI，同时保持以数学推理为核心的专门学术身份。

该基准覆盖代数、几何、数论、概率等竞赛数学主题，并提供完整解题过程。

该系统把证明搜索整体表述为端到端强化学习问题，并引入回溯机制，使智能体能够放弃预测为死路的推导并从更有希望的分支继续搜索。最终证明在 HOL4 内构造，因此仍接受证明助手内核检查。

该方法从内核级证明项中提取自监督目标，并与 tactic prediction 一起训练。

OpenAI 研究者 Stanislas Polu 与 Ilya Sutskever 在形式数学文本上训练生成模型，并将其整合进 Metamath 的证明搜索。该工作把定理证明表述为序列生成任务，并展示了学习式生成模型可以向既有形式数学库贡献可用的证明产物。

该项目把在线 tactic 学习、证明搜索与 package-aware instrumentation 结合起来，使机器学习辅助直接存在于证明助手工作流中，而不是停留在独立的 benchmark 实验里。

该基准从公理出发生成合成不等式证明，并系统改变训练与测试分布的属性，使研究者能够区分近似记忆式成功与不同形式的分布外定理证明泛化。

IsarStep 将声明式 Isar 证明转换为序列到序列样本，并移除其中的中间命题。任务要求模型重建连接前后证明状态的语义桥梁；作者评测了 Transformer 类基线，并设计面向长证明上下文的分层架构。

Skip-tree 不只遮蔽扁平 token 序列，而是从结构化数学表达式中移除一个子树并要求模型重建，从而促使表示学习利用形式数学的组合结构。

该工作把数学语篇理解明确表述为检索问题，而不仅是答案生成问题。其数据集记录 ProofWiki 中 conjecture、定义与支持命题之间的关系，并通过基线方法及后续图模型实验衡量模型恢复证明相关参考资料的能力。

该系统从既有形式数学中学习，生成额外的定理—证明对，再把合成语料反馈到证明器训练中，而不是仅依赖稀缺的人工证明轨迹。

CoqGym 从开源 Coq 项目中抽取证明状态、环境、目标、tactics 与证明树，并通过可编程交互层暴露这些信息。ASTactic 从该语料学习生成证明步骤，并基于运行时语法组合 tactics，而不是仅依赖预先固定的完整 tactic 列表。

HOList 对 HOL Light 进行工程化封装，使学习系统能够通过机器学习环境与证明状态和 tactics 交互。其 benchmark 将 core、complex 与 Flyspeck 语料中的定理陈述整理为训练、验证和测试划分；DeepHOL 则提供神经证明器与强化学习循环，用于持续生成新的成功证明轨迹。

原始版本为每个模块提供数百万规模的生成式问答样本，并在常规测试划分与外推设置上评估当时的序列到序列神经网络。配套开源生成器使研究者能够复现并扩展任务分布，而不仅依赖固定的静态题目列表。

GamePad 对 Coq 进行工程化封装，使证明状态、证明步骤、中层与内核级项以及证明树都能表示为 Python 数据结构。轻量级 coqtop wrapper 允许学习代码发送 tactics 并接收解析后的证明状态，公开工具还支持从 Mathematical Components 的 odd-order 工程中抽取数据。

该系统反复执行证明搜索模拟，把成功与失败的尝试转化为学习信号，并重新训练后续搜索所使用的引导策略。方法在大型形式数学问题语料上进行评测，重点是学习式搜索控制，而非针对具体定理手写启发式规则。

作者通过将 Mizar 陈述 informalize 为类似 LaTeX 的数学文本，构建大规模对齐语料，并训练序列到序列翻译模型重建形式语言。研究比较多种神经翻译配置，并通过案例分析模型能够正确恢复哪些数学结构。

Mathlib 将社群编写的 Lean 定义、定理、证明与 tactics 组织为共享数学库，逐步覆盖代数、分析、拓扑、数论等领域；统一 API 与协作审查实践使形式化成果能够相互复用，而非停留在彼此隔离的项目中。

TacticToe 从 HOL4 中记录 tactic 级证明信息，学习在新目标状态下哪些证明动作更有希望，并直接在高阶逻辑环境中搜索完整 tactic 序列，而不是把每个问题都翻译到一阶逻辑。2017 年系统采用改进 A* 风格搜索并结合 tactic prediction 与小规模 hammering；后续扩展实现进一步发展搜索机制，相关代码至今仍可在 HOL4 仓库中检查。

HolStep 从 HOL Light 证明中抽取中间陈述与 conjecture，对文本表示进行规范化，并把实际使用的证明步骤与负样本配对。该发布定义 conditioned 与 unconditioned proof-step classification 等任务，并提供基线代码，使研究者能够在统一的形式数学语料上比较学习式表示与相关性模型。

该系统从成功自动证明的 clause-level 轨迹中学习，并在 saturation-style proof search 中对生成的 clauses 进行排序。由于神经网络评估慢于人工设计启发式，作者采用混合引导与 two-phase search：先利用学习模型改善搜索轨迹，再由更快的传统启发式完成后续证明尝试。

该系统从对齐语料中学习如何解析有歧义的数学记号，再使用形式语义约束排除语法上合理但类型不成立或缺乏支持的解释。由此形成统计学习与符号推理结合的混合流程：学习模型提出形式结构，类型检查和定理证明机制帮助筛选与验证候选。

Holophrasm 将 Metamath 陈述解析为树结构，训练用于证明步骤生成与证明状态评估的神经模型，并与候选证明树搜索结合。公开版本包含模型训练与证明搜索代码、保存的证明结果，以及通过 Metamath verifier 重放和检查生成证明的说明。

DeepMath 使用循环与卷积神经架构编码猜想和候选前提，并学习判断某个前提是否有助于目标定理。该工作把大型形式证明语料转化为神经相关性模型的训练数据，使表示学习成为自动定理证明流程中的核心组件之一。

AITP 2016 明确将自身定位为讨论如何把 AI 与推理方法用于大规模数学和科学语料的论坛。首届议程设置了面向 ATP / ITP 与数学的 AI、非形式与半形式数学理解、现代 AI 方法等专题，并包含投稿报告。官方系列记录显示会议从 2016 年起持续每年举办至 2026 年。

项目聚焦大型复杂理论、从推理轨迹学习、演绎与学习之间的反馈循环，以及跨多种数学表示风格积累推理知识。

Lean 在一个开放平台中结合小型证明检查内核、富表达力的依赖类型理论、交互式证明开发与可扩展自动化，并同时面向形式化数学与验证任务。

完成后的工程同时形式化克卜勒猜想证明的数学文本与大型计算部分。

系统把快速学习式相关性方法扩展到约 15 万条 MML 公式，并部署到 MizAR 在线推理服务。

用户可以上传 HOL Light 工程，并让服务使用学习式相关性模型、并行 ATP 组合与决策过程处理新猜想。

项目在形式化定理本身的同时，建立了覆盖群论、线性代数、Galois 理论及实/复代数数的大规模数学库。

Sledgehammer 自动选择 Isabelle 相关事实，将证明义务翻译给外部 ATP，并利用返回结果帮助构造由证明助手检查的证明。

竞赛提供统一的 Mizar 衍生问题、公开规则与总资源预算，使学习、前提选择和其他大型理论推理策略能够直接比较。

系统反复从已有证明训练相关性模型，在筛选前提上调用自动证明器，并把新找到的证明纳入后续学习轮次。

该形式化把组合论证与计算机分类检查都纳入 Coq，使正确性依赖通用证明助手验证机制，而非四色定理专用外部程序。

项目计划同时形式化 Hales 证明中的书面数学论证与计算机计算部分，最终主要使用 HOL Light 与 Isabelle 完成。

HR 搜索数学概念空间、评估概念的有趣程度，并利用生成概念继续驱动例子、分类与猜想探索。

自动搜索在一个数十年未解决、长期接受人类与机器尝试的问题上产生了紧凑的等式推导。

各系统在共享计算环境与标准化定理证明问题上评测，使性能比较更可复现、更透明。

QED 是领域建构愿景而非单一软件发布，主张围绕共享形式数学知识开展广泛协作。

TPTP 以统一格式整理 ATP 测试问题，并建立领域分类与版本发布规范，使定理证明器能够在可比较输入上进行测试。

Metamath 将极小验证器与显式证明对象分离，使大型形式数学语料可以由最小可信机制进行检查。

Isabelle 利用高阶合一与通用元逻辑架构编码多种对象逻辑，并通过 tactics 与 tacticals 提供自动化。

HOL 结合小型可信逻辑基础、ML 编程与 tactics/tacticals，在高阶逻辑中支持目标驱动的交互式证明。

Nuprl 将构造类型论、refinement 式证明开发、tactics 与证明的计算解释结合起来；完整证明可以用于提取满足形式规格的程序，从而在同一环境中连接定理证明、形式数学与 verified programming。

Graffiti 评估图不变量之间的候选关系，保留在已知图中没有反例的陈述，并用启发式删除平凡或重复猜想。

该系统为 Calculus of Constructions 中的证明提供机器检查，并经过持续演化成为 Coq，后更名为 Rocq。

Edinburgh LCF 不再依赖保存完整证明对象，而是通过受限的抽象接口产生 theorem 值，其构造操作对应公理与推理规则。用户可以在有类型函数式语言 ML 中编写高层证明过程，并利用 tactics 与 tacticals 复用和组合反向证明策略。

AM 维护潜在有趣数学任务的 agenda，并利用通用启发式决定下一步探索哪些概念、例子与猜想。

该方法把初等几何代数化：将几何构型编码为多项式方程，并把定理证明转化为符号多项式推理。吴文俊在 Ritt 特征列思想与构造性消元基础上发展出机械化证明路线，并能显式处理退化情形。后续计算机实现证明了多项非平凡几何定理，使代数式自动几何推理成为长期研究方向。

Mizar 发展形式数学语言、检查器与数学库模式，目标是形成可累积的计算机可验证数学体系。

PLTP 面向基于归结的一阶证明器难以处理的递归程序性质，采用以化简与归纳为核心的专门证明过程。

Stanford LCF 允许用户提出证明目标、分解子目标，并通过化简与推理命令构造由机器检查的形式推导。它早于 Edinburgh LCF 中可扩展的 ML 元语言、抽象 theorem 类型与可编程 tactics。

MACSYMA 在可交互、可扩展系统中整合有理函数、代数化简、微积分及相关符号运算。

Automath 以高度显式的有类型形式语言表示定义、命题与证明，使计算机能够检查推导的正确性。

该方法通过合一处理代换，并使用统一的归结推理模式，取代早期机器定理证明中效率较低的交替过程。

SAINT 将积分表示为搜索问题，利用经验规则选择变换与代换，把积分逐步化为可求解形式。

系统把符号演绎与几何信息结合，用于剪除不合理的证明路径，展示了早期的领域知识驱动启发式推理。

系统编码逻辑表达式并搜索允许的变换空间，利用启发式优先探索更有希望的分支，而非完全穷举。

该提案并未建立独立的 AI4Math 领域，但确立了更广义的 AI 研究框架，而数学推理很快成为检验机器智能的早期核心场景之一。