江蘇
★置頂zzllrr小樂公眾號，追蹤《小樂數學科普》系列報道！
加州大學洛杉磯分校的一支計算機科學家與數學家聯合團隊，獲得了美國國防高級研究計劃局（DARPA）為期三年、總額500萬美元的資助，用于開發人工智能工具，徹底變革數學發現的提出、形式化與驗證方式。
“指數化數學”（Exponentiating Mathematics）項目旨在通過研發一款可提出并證明實用抽象概念的AI協作工具，大幅加速純數學領域的研究進展。
圖源：美國國防高級研究計劃局（DARPA）
作者：加州大學洛杉磯分校薩穆埃利工程學院 2026-5-7
譯者：zzllrr小樂（數學科普公眾號）2026-5-29
求喜歡
該項目名為ALPHA（Accelerated Formal Proof Synthesis with Neuro-Symbolic Automation，基于神經符號自動化的加速形式化證明合成），由加州大學洛杉磯分校薩穆埃利（Samueli）工程學院計算機科學系主任王瑋（Wei Wang）教授牽頭。
其他ALPHA 項目核心成員包括：
安德里亞?貝爾托齊（Andrea Bertozzi）：
數學、機械與航空航天工程杰出教授，加州大學洛杉磯分校貝齊?伍德?納普（ Betsy Wood Knapp ）創新與創意講席教授
張凱崴 （Kai-Wei Chang）：
計算機科學系副教授
彭楠赟 （Nanyun Violet Peng）：
計算機科學系副教授
阿米特?薩海（Amit Sahai）：
計算機科學與數學教授，賽門鐵克計算機科學講席教授
陶哲軒（Terence Tao）：
數學教授，詹姆斯與卡羅爾?柯林斯（ James and Carol Collins ）講席教授，純數學與應用數學研究所特別項目主任
相較于其他學科，數學領域的研究進展相對緩慢，主要源于兩大原因：其一，將復雜問題拆解為更小單元（即引理）的過程高度依賴人工、耗時費力；其二，證明這些引理需要大量專業知識與精力投入。
為攻克上述難題，ALPHA 項目將實現數學推理關鍵環節的自動化，涵蓋定理拆解、引理識別、創新證明策略生成等。該開源AI人工智能平臺可在自然語言與形式化證明系統間無縫轉換，同時保證嚴謹準確。
項目將聚焦三大核心數學領域：偏微分方程、數論、復雜性理論，目標是解決前沿數學問題，并將影響力拓展至這些核心領域之外。
通過集成 Lean、Isabelle 等開源證明輔助工具，ALPHA 將確保輸出結果的準確性，同時充分利用現有形式化數學庫與開發者社區資源。系統依托大語言模型、神經符號人工智能、代碼生成與自動定理證明領域的前沿成果，致力于打通人類直覺與機器驗證，從根本上重塑數學研究范式。
“這是連接人類直覺與機器驗證的關鍵一步，” 持有倫納德?克萊因羅克計算機科學講席的王瑋教授表示，“我們的目標是從根本上拓展數學家探索與驗證新思想的方式。”
加州大學洛杉磯分校是3月21日DARPA “指數化數學”（expMATH）計劃遴選出的13支高校團隊之一。該計劃旨在研發可充當科研協作伙伴的人工智能系統，加速純數學領域的研究突破。
參考資料
https://www.universityofcalifornia.edu/news/ucla-team-awarded-5-million-darpa-contract-develop-ai-math-advancement
https://lean-lang.org
https://isabelle.in.tum.de
小樂數學科普本月文章
小樂數學科普歷年合集
版權聲明：本文首發于微信公眾號“zzllrr小樂”的專欄《小樂數學科普》。歡迎個人轉發。如需轉載，請在“zzllrr小樂”公眾號后臺回復“轉載”，還可通過公眾號菜單、發送郵件到zzllrr@gmail.com與我們取得聯系。相關圖文音視頻內容默認遵守CC BY-NC 4.0知識共享協議，未獲作者和譯者授權，禁止用于營銷宣傳和商業目的。
·開放 · 友好 · 多元 · 普適 · 守拙·
讓數學
更加
易學易練
易教易研
易賞易玩
易見易得
易傳易及
歡迎評論、點贊、在看、在聽
收藏、分享、轉載、投稿
查看原始文章出處
點擊底部一起捐
助力騰訊公益
點擊zzllrr小樂
公眾號主頁
右上角
置頂★加星
數學科普不迷路！
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
