AxiomProver：当数学直觉遇见形式化海啸

AxiomProver：当数学直觉遇见形式化海啸

🌊 开篇：一个 24 岁女孩的"不可能"宣言

2025 年 6 月的一个深夜，Carina Hong 盯着屏幕上的 Lean 编译器，指尖在键盘上悬停。她的团队刚刚花了三个月，试图让 AI 理解"为什么三角形的内角和是 180 度"。不是计算，不是记忆——是理解。

"这太荒谬了，"她转身对联合创始人说，"人类用一张图就能讲清楚的道理，机器需要 200 行代码。"

那一刻，她意识到数学教育的终极悖论：我们教孩子"显而易见"，却教机器"每一步都必须证明"。

六个月后，AxiomProver 在 Putnam 竞赛上拿下了 120/120 分。这不是胜利，这是宣言——AI 正在学会一种全新的数学语言。

🎯 核心概念：极简定义背后的海啸

AxiomProver = Axiom（公理）+ Prover（证明者）+ X（未知变量）- 一个会写 Lean 证明的"AI 数学家"

用最直白的话说：AxiomProver 是一个能"看到"数学结构，并把它翻译成机器可验证代码的智能体。

费曼测试：五句话说清

  1. 它是个翻译官：把人类直觉（图形、类比）变成 Lean 代码（严格、完整）
  2. 它是个顽固者：不接受"显然"，每一步都要有引理、定理、证明
  3. 它是个异类：在组合题上碾压人类，在微积分上"笨拙"到可笑
  4. 它是个合作者：人类提供灵感，它负责"把灵感落地成可验证的事实"
  5. 它是个温度计：测量着"奇点"与我们的距离——不是科幻，是数学

⚙️ 架构之美：三层隐喻

表层：12 道题的数字墓碑

┌─────────────────────────────────────┐
│  2025 Putnam 竞赛                   │
│  12 道题，6 小时，120 分           │
├─────────────────────────────────────┤
│  A2：微积分证明 → 200 行 Lean 代码 │
│  B2：测度论 → 60 行正性证明        │
│  A5：排列归纳 → 2054 行，518 分钟 │
│  A3：组合博弈 → 300 行，AI 突袭   │
│  B1：几何推理 → 400 行，无图证明  │
│  A6：p 进数 → 5 小时，蛮力胜利    │
└─────────────────────────────────────┘

每一道题都是一个数字墓碑，上面刻着两种墓志铭：

人类版： "显然"、"易证"、"如图所示" AI 版： "import Mathlib"、"theorem"、"have h1 : ..."

中层：流动的数据之河

graph TD
    A[人类直觉] --> B[Carina Hong & Team]
    B --> C{AxiomProver}
    C --> D[Lean 编译器]
    D --> E[形式化证明]
    E --> F[GitHub 公开]
    
    G[Putnam 2025] --> H[12 Problems]
    H --> C
    
    style A fill:#ffebee
    style C fill:#e8f5e9
    style E fill:#fff3e0

这就是 AxiomProver 的魔法链条：人类灵感 → AI 翻译 → Lean 验证 → 公开可查。

  • 输入层：人类提供数学竞赛题目
  • 处理层：AxiomProver 进行符号推理与形式化
  • 输出层：生成可在 Lean 中验证的完整证明
  • 存储层：所有证明公开在 GitHub 上，供社区审计

底层：涌现的生态系统

AxiomProver 最深刻的洞察在于：它是一个"认知拓扑揭示器"。

graph LR
    A[人类思维] --> B[几何直观]
    A --> C[代数推理]
    A --> D[组合构造]
    
    E[AI 思维] --> F[符号遍历]
    E --> G[暴力枚举]
    E --> H[穷举搜索]
    
    B --> I[认知不匹配]
    C --> I
    D --> I
    F --> I
    G --> I
    H --> I
    
    style I fill:#fff3e0

这揭示了认知拓扑结构：人类与 AI 的思维空间是相似但不同构的流形。

📊 数据墓碑：证明的量化考古

题目人类感知AI 感知Lean 代码行数生成时间胜负手
A2简单（看图）繁琐（定义）~200-人类胜在直觉
B2简单（引理）繁琐（60+行证明）~150-人类胜在简洁
A5中等（归纳）极繁琐（记账）2054518 分钟AI 胜在耐心
A3难（组合）简单（无分支）~300-AI 胜在逻辑
B1难（几何）中等（符号）~400-AI 胜在代数
A6极难（p进）难（蛮力）高 token5 小时AI 胜在坚持
A4中等（代数）中等（几何）~500-思路不同
B4中等（图解）繁琐（枚举）1061-思路不同

这表格是一面镜子：照出了人类与 AI 的认知拓扑结构——相似但不同构。

🧠 认知拓扑：两种思维的几何

人类数学：Grothendieck 的"涨潮海"

数学家 Alexander Grothendieck 有个著名隐喻：数学研究不是"钻探石油"，而是"等待海水上涨，淹没问题"。

人类数学家：

  1. 发现模式：在混乱中看见结构
  2. 抽象概念：把模式变成定义（如"群"、"流形"）
  3. 建立理论：在抽象上构建城堡
  4. 解决特例：用理论工具处理具体问题

这是自顶向下：从一般到特殊。

AI 数学：Turing 的"暴力搜索"

AxiomProver：

  1. 生成所有可能：在搜索空间里遍历
  2. 验证每个候选：用 Lean 检查正确性
  3. 找到路径：在组合爆炸中找线性路径
  4. 输出证明：把路径翻译成形式语言

这是自底向上：从特殊到一般。

不对称性的价值

这两种思维不可比较，但可互补。

Carina Hong 的愿景正是：人类提供灵感，机器负责验证，两者螺旋上升。

🔮 未来推演：奇点的三次逼近

第一次逼近：GPT-5.2 Pro 的"离谱"

波兰数学家 Bartosz Naskręcki 观察 GPT-5.2 Pro：

"面对非平凡问题，很难找到真正能让 AI 卡死的点。一到两小时的交互，模型就能把答案推出来。"

他的震撼是半开玩笑的：

"要么 OpenAI 背后有一支「全天候的小精灵与顶尖数学家团队」在实时代打，要么模型已经具备非常扎实的能力。"

这是一种 "图灵测试"的反向版本 ：不是机器冒充人类，而是人类怀疑机器背后有人。

第二次逼近：AxiomProver 的"蛮力优雅"

AxiomProver 在 A6 题上的胜利是蛮力的胜利：

  • 5 小时，token 用量第二高
  • 用"特别笨拙、但确实有效的方法"做 p 进数展开
  • 人类数学家方向对了，但卡在最后一步

这揭示了AI 的"暴力美学"：当灵感枯竭时，耐力就是创造力。

第三次逼近：Terence Tao 的"里程碑"

陶哲轩说 AI 解决了 Erdős 问题，是里程碑。他不是夸张——Erdős 问题以"开放、难、需要新想法"著称。

如果 AI 能自主解决 Erdős，那千禧年难题（P vs NP, Riemann 猜想）可能真的在可预见的未来。

但，Tao 也谨慎：里程碑 ≠ 奇点。奇点需要自我改进的闭环，目前 AI 还是工具，不是主体。

🎭 争议与反思：在欢呼声中听见沉默

争议 1：这是不是"真正的理解"？

批评者说：

"AI 只是在模式匹配，它不知道'为什么'。"

支持者反驳：

"人类数学家也做模式匹配——我们叫它'直觉'。"

真相可能在中间：AI 的理解是句法的（syntactic），人类理解是语义的（semantic）。但句法足够复杂时，行为上不可区分。

争议 2：Lean 是否"足够数学"？

Lean 的形式化有代价：

  • A2 题：60 行证明"正性引理"
  • A5 题：2054 行，518 分钟

这暴露了形式系统的"税负"：把直觉翻译成机器语言，需要缴纳"繁琐税"。

但这也是Lean 的价值：它强迫你检查每个"显然"。

争议 3：AI 会取代数学家吗？

Carina Hong 的回答很清晰：

"我们不需要硬攻每一个问题。人类直觉 + 机器验证 = 涨潮的海。"

这是"人机共生"的宣言：

  • 人类：灵感、抽象、美学判断
  • AI：验证、枚举、 exhaustive search

不是取代，是分工。

📖 结语：在形式与直觉之间

费曼会问："如果 AxiomProver 消失了，我们会失去什么？"

答案是：一种全新的数学对话方式。千百年来，数学是"人类说，人类听"。现在，出现了第三种声音——机器说，人类验证，机器再反馈。

这像三体人的交流：思想透明，即时验证，无需欺骗。

AxiomProver 做到了。它让数学从"独白"变成了"对话"。

🔗 附录：快速参考

概念人类方式AI 方式隐喻
证明灵感 → 构造枚举 → 验证建筑师 vs 施工队
难度无灵感 = 无解高 token = 难解诗人瓶颈 vs 算力瓶颈
几何图形直观符号代数画家 vs 代数学家
组合构造巧妙无分支搜索魔术师 vs 穷举器

项目：https://axiommath.ai 证明：https://github.com/axiommath/proofs 创始人：Carina Hong (@CarinaLHong) 协议：AI + Human Collaboration

"数学不是聪明的符号游戏，而是对真相的耐心挖掘。" —— 从 Hilbert 到 Lean，再到 AxiomProver

这正是 AxiomProver 的哲学：在形式与直觉之间，架起一座桥。

← 返回目录