2026-03-19 00:47 UTC
更自動化的證明生成方法，或許能更高效地完成從 A 點到 B 點的主要目標，但這往往是以犧牲「次要目標」為代價的——特別是當這些方法被應用於大規模、非互動式的流程時。這就像汽車的駕駛或乘客雖然抵達了目的地，卻對沿途有趣的地理特徵毫無察覺。
除其他因素外，這也使得此類證明通常不適合在傳統期刊上發表。因為在 AI 生成的證明中，那種描述通往證明之路的「敘事性」——包括其在先前研究背景下的地位、從證明過程中所學到的教訓，或是建議的未來方向——幾乎完全缺失。
或許有人會嘗試進一步「升級」AI 的能力，為 AI 生成的數學增添這類功能，以便產出適合在傳統期刊發表的文章；但在我看來，這就像是試圖改裝汽車，好讓它們塞進為行人設計的街道裡。同理，讓 AI 模型去達成與人類成就表面相似的壯舉，可能在變得越來越令人驚嘆的同時，也變得越來越毫無意義——這就好比證明一輛汽車可以「贏得」馬拉松，僅僅是因為它跑完賽程的時間比任何人類跑者都短得多。(3/5)
Replies (1)
-
@typingmonk@g0v.social 2026-03-19 00:47
對我而言，更好的前進方向是開發一套對機器友善的新型數學基礎設施——類比於現代道路、鐵路或高速公路——這套設施應與現有以人為本的通路和建築相輔相成，而非取而代之，如此才能更充分地發揮新技術在效率與規模上的優勢。 「大規模數學挑戰賽」（Large-scale mathematical challenges）便是這種新基礎設施的一個例子——這有點像是一條「高運量貨運走廊」——在其中，一套經由專家精心策劃、具備數學意義的任務或問題被陳列出來，供各方參與者以任何手段（或任何程度的 AI 輔助）去解決；而證明結果則透過某種高效且可信的流程（例如透過形式化證明輔助工具）進行驗證，以確保能安全處理這類挑戰所產生的大量數據。 或者，我們可以使用自動化方法，為文獻中現有的眾多結果開發一個大規模的「低品質證明圖書館」，將其作為人類的起點（或許再輔以專門的 AI 工具），進而創造出具有額外教學意義、風格美感或藝術價值的「高品質證明」。延續交通的比喻，這就像是沿著高速公路系統開往國家公園裡一個平凡無奇的停車場，接著再步行幾英里，前往風景優美的目的地。(4/5)