AxiomProver是一個基於Lean的AI自動推理系統，由華人女學霸Carina Hong初創打造。在2025年，該系統在Putnam數學競賽中獲得了滿分成績，12道題全部答對。此外，它還解決了Erdős問題集中的第124題和第481題。
2025年，Axiom Math團隊完成了6400萬美元融資，創始人洪樂潼（Carina Hong）放棄了博士學位，全職投入創業。
研發背景,核心團隊,核心技術,重要事件,
研發背景
AxiomProver系統的研發始於其創始人洪樂潼對形式化驗證語言Lean的探索。2024年秋天，一種名為Lean的語言進入她的視野。與自然語言不同，Lean語言是一個可以自驗證的數學程式語言。洪樂潼打了個比方：“如果用英語寫出數學證明，我沒辦法知道一個5000行的證明是否正確，需要找高水平的專家驗證。但Lean是自驗證的，只要跑通了就是對的。”
2025年1月，在美國最大的數學家聚會——2025年聯合數學會議(JMM, Joint Math Meeting)上，洪樂潼見到了許多做Lean語言的數學家。她意識到，“AI數學家”有可能從科幻變成現實。2025年10月，在Axiom Math完成6400萬美元融資後，洪樂潼全職投入了創業。
核心團隊
AxiomProver由24歲華人女學霸洪樂潼（Carina Hong）創立並領導。團隊核心成員僅4人，總人數不足10人。
AxiomProver解決了懸置30年和45年的埃爾德什問題#124和#481，並在Putnam數學競賽中取得滿分成績。
核心技術
AxiomProver基於完全可驗證的定理證明輔助工具Lean語言構建。系統採用自主多智慧型體集成架構，並以Claude Opus 4.5作為基礎模型。其核心推理能力體現在能將人類數學直覺轉化為嚴格的形式化證明，且在部分問題上能提供與人類不同的創新解題思路，例如將代數問題轉化為幾何視角。
重要事件
2025年12月3日，AxiomProver在無人干預下，分別用1天和5小時解決了懸置約30年的埃爾德什問題#124和懸置45年的#481，並完成了形式化驗證。
2025年，在威廉·洛厄爾·普特南數學競賽中，AxiomProver在競賽結束前已解決8道題，賽後共解決9道題；按往年成績估算，此表現可位列前五名（Putnam Fellow）。團隊隨後公開了其針對該競賽全部12道題目的Lean證明。
2026年，開源系統Numina-Lean-Agent復現了AxiomProver在Putnam 2025中解決全部12道題目的表現，並在部分題目（如B1）上生成了更簡潔的證明，其結果與AxiomProver持平。
