Axiom CEO Carina Hong 讨论他们的 AI 数学家如何结合生成与验证，在普特南考试中取得最高分，以及摇滚乐如何影响她的创业之旅。
Axiom's CEO Carina Hong discusses how their AI mathematician combines generation and verification, achieving top scores on the Putnam exam, and how rock and roll influences her startup journey.
要点 · TL;DR
Axiom 结合生成与验证，打造自我改进的推理引擎。 Axiom combines generation and verification for a self-improving reasoning engine.
像 Lean 这样的形式语言为可靠的 AI 证明奠定自然语言基础。 Formal languages like Lean ground natural language for sound AI proofs.
Axiom 构建了一个结合生成与验证的自我改进推理引擎，从 AI 数学家开始。 Axiom builds a self-improving reasoning engine combining generation and verification, starting with an AI mathematician.
像 Lean 这样的形式语言为自然语言提供基础，使确定性和概率性系统协同工作。 Formal languages like Lean ground natural language, enabling deterministic and probabilistic systems to work together.
该系统包括证明器、猜想器和知识库，自动形式化将它们编织在一起。 The system includes a prover, conjecturer, and knowledge base, with auto-formalization weaving them together.
Axiom 在 Putnam 考试中取得了最高分，展示了结合形式与非形式推理的力量。 Axiom achieved top scores on the Putnam exam, demonstrating the power of combining formal and informal reasoning.
该技术可应用于硬件/软件验证、代码迁移和安全关键领域。 The technology has applications in hardware/software verification, code migration, and safety-critical domains.
反共识 · Contrarian takes
将非形式模型 Scaling 到数学 AI 不可行；形式验证对于可靠的证明至关重要。 Scaling informal models to math AI is not viable; formal verification is essential for sound proofs.
AI 证明可能不优雅，但简化后可能收敛到类似人类的直觉，如同拉马努金的工作。 AI proofs may be ugly but can converge to human-like intuition when streamlined, like Ramanujan's work.
自动形式化比证明更难；在没有解决方案的情况下正确形式化陈述具有挑战性。 Auto-formalization is harder than proving; correctly formalizing statements without solutions is challenging.
顶尖数学家与普通学者之间的差距大于本科生与普通学者之间的差距。 Top mathematicians have a bigger gap to average academics than undergrads to average academics.
创业文化应像地下摇滚乐队一样保持饥饿感和不适感，避免自满。 The startup culture should preserve hunger and discomfort like underground rock bands, avoiding complacency.
本期章节 · Chapters（共 20）
0. Axiom简介及其使命Introduction to Axiom and its mission
1. 简单示例演示Axiom运作How Axiom works on a simple example
2. 从学术之路到创业创始人From academic path to startup founder
3. 人工智能与数学的未来Future of mathematics with AI
4. 语言模型与人类的难度层级Difficulty hierarchy for LMs vs humans
5. AI证明的可验证性Verifiability of AI proofs
6. AI作为数学家的协作者AI as a mathematician collaborator
7. 展示证明树Demonstrating the proof tree
8. 理解问题A3Understanding problem A3
9. 主持人尝试解答A3Host's attempt at A3
10. A3问题中Bob的获胜策略Bob's winning strategy in A3 problem
11. 形式化验证的应用与里程碑Applications and milestones of formal verification
12. AI验证与编码的三个层级Three tiers of AI verification and coding
13. 交互反馈与自动形式化Interactive Feedback and Autoformalization