LLM框架用於發現重大數學猜想：AI探索下一個黎曼猜想

重大數學猜想的提出，長期以來被視為數學智慧的最高體現之一。無論是黎曼猜想、哥德巴赫猜想，還是千禧年難題，它們的誕生往往來自少數數學家在長期思考中的靈光一現或深刻洞見。這種對專家直覺的嚴重依賴，使得猜想發現難以被系統化地複製、評估和驗證。arXiv 上最新發布的一篇論文嘗試改變這一現狀：研究人員提出了一套以大語言模型（LLM）為核心的三階段流水線，用於自動生成並驗證具有實質數學潛力的猜想，目標被明確稱為“下一個黎曼猜想”級別的探索。

這套流水線的第一階段是區域搜尋（region search）。與之前一些從零開始隨機生成命題的做法不同，該階段要求模型從顯式的區域性證據模組出發。所謂區域性證據，可以理解為一些在特定數學領域中已經被驗證為真、或具有較強支援的小範圍事實。模型在這些證據的引導下，在某個數學子領域中搜尋可能成立的候選猜想，從而避免完全盲目的生成。第二階段是反思性驗證（reflective validation）。系統會從基礎性（foundationality）、新穎性（novelty）和潛在重要性（potential significance）三個維度對每個候選進行內部批判。基礎性考察候選命題是否紮根於核心數學結構，新穎性考察它是否區別於已有結果，潛在重要性則衡量一旦被證明，它對理論發展的推動作用。第三階段是形式化驗證（formal validation）。候選猜想會被交給 Lean 4 證明助手及其數學庫 Mathlib，用機器可檢查的嚴格邏輯語言重新表述。只有透過了 Lean 的解析與型別檢查，候選猜想才算在形式上獲得了合格證。

研究者用一個頗具感染力的概念概括這項工作的目的——“問題品味”（problem taste）。一個有高度問題品味的數學問題，其證明有可能重新組織一個研究領域的語言，為後續大量工作提供新的框架和工具，並對人類數學研究提供持久的幫助。換句話說，這項研究不只是想生成一堆“可能正確但無關緊要”的命題，而是希望找到那些一旦被證實就能改變領域走向的核心問題。

論文報告了二十個候選猜想的實驗結果。資料顯示，從自然語言表述到形式化檢查的過渡相當穩定：二十個候選全部透過了 Lean 4 的解析和型別檢查；全部二十個都沒有被 exact? 這一自動化策略直接吸收；也全部都沒有被 aesop 這類自動證明搜尋工具直接消解。此外，系統沒有發現這些候選之間存在顯式重複或近似重複。儘管這只是一次規模的演練，但作者認為，這表明流水線有能力在保持一定質量門檻的同時產出多樣化的候選猜想。

該論文由 Alizer Wong 與其他七位作者共同完成，全文二十五頁，包含一幅圖，於 2026 年 4 月 19 日提交至 arXiv，編號為 arXiv:2607.28632 [cs.AI]，並配有 DataCite 生成的 DOI（https://doi.org/10.48550/arXiv.2607.28632）。投稿歷史顯示，第一版（v1）由 Zixin Zeng 提交，檔案大小約 1,319 KB。論文並未聲稱已經發現了真正的“下一個黎曼猜想”，而是提出了一套可復現的方法論，讓 AI 能夠以更嚴格、更透明的方式參與數學發現。對於關注 AI for Math 的研究者和工程師而言，這項工作展示了大語言模型與形式化驗證工具結合的一種新正規化，也提醒我們：未來數學中的創造性工作，可能會越來越多地由人類與 AI 共同完成。