WIRED 在 2026 年 2 月 4 日报导，AI 数学新创 Axiom 宣称其系统在近几周内解出 4 个先前未解的数学问题。约 5 年前，Dawei Chen 与 Quentin Gendron 在代数几何研究中遇到一个依赖数论奇特公式的关卡，最终只能以猜想形式发表；Chen 后来花数小时用 ChatGPT 尝试仍无果。上个月在华盛顿特区的一场数学会议招待会，Chen 把问题告诉 Ken Ono；隔天 Ono 以 Axiom 的 AxiomProver 产生的证明回复，之后与 Axiom 合作整理并张贴于 arXiv（2602.03722）。Axiom 表示，系统找到了与 19 世纪数值现象的连结，生成证明并自行验证，指出人类先前忽略的关键。

Axiom 的方法是把大型语言模型与专有推理系统结合，让 AxiomProver 在可形式化验证的框架中推导出可证明正确的结果；它使用专门的数学语言 Lean 来验证证明，而非仅在文献中检索。Axiom 也将其作法与 2024 年 Google 展示的 AlphaProof 类系统相提并论，并声称 AxiomSolver 纳入更新技术与多项进展。另一份 arXiv 论文（2602.03716）描述其对 Fel’s Conjecture 的解答，主题涉及 syzygies；该猜想与 Srinivasa Ramanujan 超过 100 年前笔记中的公式相关。报导称此案中 AxiomProver 从头到尾自行构造证明并即时验证；Harvard Business School 的 Scott Kominers 将其评为同时具备全自动、可验证与数学上的优雅。

其余两个解答中，第三个涉及数论中所谓「dead ends」的机率模型，第四个借用了最初为攻克并最终解决 Fermat’s Last Theorem 而发展的工具。Axiom 与 Ono 将这些结果定位为 AI 数学推理能力的持续上升，但也承认尚未解出该领域最著名或最具奖金的问题。Axiom 的 CEO Carina Hong 指出，数学是检验推理的「sandbox」，而同类技术可外溢到高商业价值场景，例如用 AI 验证程式码在特定攻击模型下的可靠性与可信性，以提升资安韧性。Ono 将此描述为证明定理的新典范，并试图理解「aha moments」能否变得可预测；Chen 以计算机未使数学家忘记乘法表作比，将 AI 描述为可能拓展研究地平线的工具。

WIRED reported on Feb 4, 2026 that the AI math startup Axiom says its system solved 4 previously unsolved problems in recent weeks. About five years earlier, mathematicians Dawei Chen and Quentin Gendron hit a roadblock in algebraic geometry: their argument depended on a strange number-theory formula they could not justify, so they published the idea as a conjecture. Chen later spent hours prompting ChatGPT without success; at a Washington, DC conference reception last month he told Ken Ono, and the next morning Ono returned with a proof produced by Axiom’s AxiomProver, later written up and posted to arXiv (2602.03722). Axiom says the system linked the problem to a numerical phenomenon first studied in the 19th century, generated a proof, and verified it, surfacing a key step humans had missed.

Axiom’s approach combines large language models with a proprietary reasoning system intended to reach provably correct results; AxiomProver can verify proofs in the specialized mathematical language Lean rather than merely searching the literature. The company frames its work against similar efforts, including Google’s 2024 AlphaProof, and says AxiomSolver incorporates newer techniques and significant advances. A second arXiv paper (2602.03716) describes a solution to Fel’s Conjecture about syzygies, tied to formulas from Srinivasa Ramanujan’s notebooks more than 100 years ago. In this case, the report says AxiomProver constructed the proof end to end and had it instantly verified; Harvard Business School professor Scott Kominers called the result notable for being fully automated, verifiable, and mathematically elegant.

The remaining two Axiom solutions include a third proof involving a probabilistic model of “dead ends” in number theory and a fourth drawing on tools originally developed to attack and ultimately solve Fermat’s Last Theorem. Axiom and Ono present the set as evidence of steadily improving AI mathematical reasoning while noting it has not yet cracked the field’s most famous or lucrative problems. CEO Carina Hong describes math as a test-ground “sandbox” and argues the same verification-centered methods could transfer to high-value domains, such as making software more resilient to cybersecurity attacks by proving code reliable under specified assumptions. Ono calls this a new paradigm for proving theorems and an opportunity to study whether “aha moments” can be made predictable; Chen likens the shift to calculators not erasing multiplication tables, framing AI as a tool that can broaden mathematical research horizons.