一、从 Vibe Coding 到 Vibe Math
"Vibe Coding" 由 Andrej Karpathy 于 2025 年提出，指程序员完全交由 AI 处理代码实现细节、人类仅提供方向意图的新型编程范式。数学研究能否实现类似的"Vibe Math"？传统观点认为数学比编程更难 AI 化——证明正确性难以自动验证、需要深层创造性思维、每个问题都具有独特性。然而，形式化验证（Formal Verification）的出现改变了这一判断：它将数学证明转化为计算机可逐步检查的代码，编译通过即证明正确，编译失败则暴露逻辑漏洞。形式化验证相当于数学的"编译器"，使 Vibe Math 成为可能。
二、AI 数学能力的飞跃
AI 的数学能力在两年内实现了从"做不了竞赛题"到"金牌水平"的跨越。2024 年 7 月，AlphaProof 与 AlphaGeometry 2 获得 IMO 银牌；2025 年 7 月，Gemini Deep Think 达到 IMO 金牌标准并斩获 ICPC 世界总决赛金牌。在基准测试方面，MATH benchmark 上 o3 达到 96.4%，FrontierMath（由 60 余位研究数学家出题、含 Fields 奖得主审核的前沿问题集）上，模型表现从 2024 年 11 月的不足 2% 跃升至 2026 年 3 月的 50%。
更具里程碑意义的是，AI 开始解决真正的数学开放问题：Erdős Problem #728（阶乘整除猜想）由 Barreto 与 ChatGPT-5.2 给出证明并已在 Lean 中形式化验证；Will Brian 与 Paul Larson 提出的 Ramsey 超图猜想（作者 7 年未解）被 GPT-5.4 Pro 完整证明。FirstProof 挑战中，11 位顶级数学家（含 Fields 奖得主 Martin Hairer）出题 10 道研究级难题，DeepMind 的 Aletheia 系统解出 6/10，其架构融合 Gemini Deep Think、自然语言验证器与搜索浏览能力，已自主扫描 700 个 Erdős 开放问题并解决 4 个。
三、形式化验证
形式化数学的核心思想是将证明写成计算机可检查的代码，Lean（Microsoft Research）、Coq、Isabelle 等工具充当"编译器"。其重要性源于数学论文的错误率问题——Fields 奖得主 Voevodsky 曾发现自己 1989 年的论文存在严重错误，这促使他投入 Univalent Foundations 和 Coq 形式化，并坦言"我再也无法信任非形式化的证明"。Mathlib 作为 Lean 4 的数学标准库，已积累 100 万+ 行代码，覆盖代数、分析、拓扑、数论等领域，相当于一部机器可读的数学百科全书。
形式化验证的重大成就包括：2005 年四色定理（Coq）、2017 年 Kepler 猜想（HOL Light + Isabelle）、2023 年 PFR 猜想（Tao 等，3 周完成）、2026 年 E₈ 球填充与 24 维 Leech 格（Math Inc. 的 AI 系统 Gauss 独立完成）。自动形式化的意义在于让 AI 承担繁琐的代码转换工作——自然语言证明仅需 3 行，Lean 4 形式化却需约 10 行，AI 可将前者自动翻译为后者并通过编译器验证，形成"生成→验证→迭代修复"的闭环。
四、技术演进：从专用模型到 Agent
AI 数学推理经历三个时代。**时代一（2020–2023）**为专用模型加树搜索：GPT-f 首次用 Transformer 做 Metamath 证明，AlphaProof 以 AlphaZero 式自我对弈获 IMO 金牌，核心公式为"推理能力 ≈ 模型质量 × 搜索预算"，但缺乏高层证明规划。**时代二（2023–2025）**为 Informal 与 Formal 混合：Draft, Sketch, and Prove 范式先用自然语言"打草稿"再映射为形式化代码，DeepSeek-Prover-V2 在 miniF2F 达 88.9%，核心洞察是"80% 的难度在找到正确策略，而非写 tactic"。**时代三（2025–）**进入 Agent 工作流：从"一个模型解一道题"转向"多角色协作"，Plan Agent 负责分析路径、Informal Agent 生成草稿、Lean Agent 翻译代码并调用 Mathlib 搜索等工具，代表系统包括 Archon、Gauss 与 Aletheia。三个时代并非替代关系，而是叠加演进。
五、AI 发现新数学
AI 发现新数学的范式从 2021 年的 ML 引导直觉（Davies 等，Nature），演进至 2024 年的 LLM 加进化搜索（FunSearch 发现 cap set 问题新下界），再到 2025 年的 Agent 进化代码库（AlphaEvolve 改进 70 余个数学常数的已知界）。共同模式为：AI 提出候选→自动评估验证→迭代优化→人类数学家确认。AI 不直接证明定理，而是帮助数学家"看到"数据中隐藏的规律。
六、Vibe Math 工作流与未来展望
未来数学家的工作流将呈现"Advisor 模式"：人类引导 AI 进行迭代式 Vibe Proving 循环，采用 Balanced Prompting（同时要求证明与反驳以防止确认偏误）、Code-assisted Verification 等策略。自动形式化工作流分为六步：AI 分析 LaTeX 提取定理→搜索 Mathlib 复用定理→生成形式化代码→Lean 编译器验证→失败则分析修正→交付零错误的 PR 或论文。人类的角色从"写证明"转向"选题、审查、填补最难的 gap"。
关于"数学家是否会被替代"，Terence Tao 的观点颇具代表性："AI 不会取代数学家，但使用 AI 的数学家将取代不使用 AI 的数学家。"数学的价值既在于结果，也在于理解的过程——AI 正在改变两者的比例。当前（2024–2026）竞赛解题、自动形式化、初步研究辅助已实现；近期（2026–2028）将走向端到端论文形式化与 AI-human 协作常态化；远期（2028+）则可能迎来自主数学发现、形式化成为发表标准、数学教育革命等深层变革。Vibe Math 不是科幻，它正在发生——问题不是 AI 能不能做数学，而是我们如何与 AI 一起做数学。
