區塊鏈基礎設施平台 Eclipse 近日發布研究，探討人工智慧（AI）在數學發現中日益重要的角色。這項研究計畫檢視了先進的 AI 系統如何透過「自動形式化」（autoformalization）的過程，協助數學家解決複雜問題。自動形式化指的是將人類可讀的證明轉換為機器可驗證的數學格式。

研究強調，AI 生成的證明可能會暴露數學家在定義成功、新穎性和原創性時存在的模糊性。隨著 AI 系統越來越多地生成數學證明，重新發現、漸進式改進和真正創新之間的傳統界限變得模糊，需要新的方法來衡量 AI 輔助研究的重要性。

這項名為 GPT-Erdos 的計畫，將先進的 AI 模型應用於數學家保羅·艾狄胥（Paul Erdős）最初提出的一些開放性數學問題。實驗產生了部分解決方案、先前成果的重新發現，以及對現有技術的新觀點。

Eclipse 的研究人員觀察到，AI 生成的證明通常滿足形式要求，但與人類的預期不同，突顯了數學問題中「規格欠定」（underspecification）的挑戰。

Eclipse 創辦人尼爾·索馬尼（Neel Somani）表示，他們正在探索一些方法，可以引入新的指標來衡量數學證明與完成之間的「接近程度」，從而使 AI 系統能夠識別有希望的證明路徑，即使尚未完全形式化的結果。

該研究強調，人工智慧和形式數學的結合，可能會從根本上重塑數學發現的實踐，AI 系統將作為協作者，能夠探索廣闊的概念空間並快速驗證複雜的推理。這種趨勢可能促使數學界重新評估評估數學研究的標準，並思考如何將 AI 納入數學教育和研究中。對台灣的數學教育和科研領域而言，這項研究也提供了一個契機，重新思考如何培養學生和研究人員與AI協作的能力，並探索AI在解決數學難題上的潛力。