兩個GitHub儲存庫擬公開，收錄OpenAI楊-米爾斯Lean程式碼與審查資料

楊-米爾斯工作小組（Yang-Mills Working Group）計畫將OpenAI提交的量子楊-米爾斯理論Lean程式碼與審查評估資料，分別放在兩個GitHub儲存庫公開。

Crypto Briefing於10日報導，工作小組預計在美國當地時間10日公開資料。第一個儲存庫將收錄OpenAI提交的完整Lean程式碼，第二個則放入工作小組的驗證評估資料。

工作小組在11月3日發布的第二份聲明中表示，正在檢查程式碼的定義與問題設定是否符合物理學和數學的標準，以及自然語言證明是否與程式碼一致。工作小組當時希望在11月第二週公開資料，並表示會在公開前一天通知。

OpenAI於9月9日表示，已完成一份關於楊-米爾斯理論存在性的自然語言證明；9月18日又說，另完成一份關於量子色動力學的自然語言證明。

OpenAI於10月16日完成楊-米爾斯證明的Lean形式化。Crypto Briefing報導，OpenAI同日首次聯繫諾貝爾獎得主大衛·格羅斯（David J. Gross），之後成立工作小組進行獨立審查。

OpenAI曾公開數學與電腦科學領域的AI成果，但物理學成果先交由專家審查。OpenAI在10月26日的公告中表示，工作小組將獨立作出結論，不代表OpenAI的立場。

工作小組也表示不對OpenAI負責。這項安排將提出成果的公司與審查方分開。

Lean是一種將數學定義與論證寫成程式碼的工具，能讓電腦逐步檢查證明。把自然語言寫成的解答轉為形式化程式碼後，便可依照既定規則機械式檢查每個論證步驟。

不過，程式碼在邏輯上成立，不代表它就準確證明了學界要解決的問題。如果定義或問題設定與標準不同，電腦仍可能正確證明另一個問題的答案。因此，工作小組也將檢查兩者是否一致。

量子楊-米爾斯理論是描述強作用力的量子色動力學基礎。純楊-米爾斯理論探討不含夸克的膠子交互作用；量子色動力學則包含夸克。

克雷數學研究所（Clay Mathematics Institute）的千禧年大獎難題要求證明楊-米爾斯理論在四維空間成立，並證明存在「質量間隙」。質量間隙是指基態與下一個能量狀態之間存在正值差距。

OpenAI提出的證明主張該理論存在。工作小組表示，質量間隙與夸克禁閉仍是尚待解決的問題。

工作小組在10月聲明中表示，OpenAI採用的方法以威爾遜格點正規化（Wilson lattice regularization）和巴拉班重整化群方法（Balaban's renormalization-group methods）為基礎。工作小組也指出，證明篇幅長、內容複雜，需要時間理解其方法與物理意義。

OpenAI提交的完整證明資料共1147頁。工作小組表示，若確認證明正確，將連同評估結果公開AI撰寫的完整證明資料。