OpenAI 公布 AI 在數學與理論電腦科學的十項進展

OpenAI 於 8 月 1 日公布一組由內部 Astra 模型協助取得的數學與理論電腦科學結果，覆蓋高維球堆積、編碼、群論、算術電路、量子複雜性、格密碼和極值組合等方向。官方說明，這些問題多數至少十年沒有在主要結論上取得進展；研究團隊隨後由人類整理成論文，並為每項結果提供 Lean 形式化證書。公開倉庫也列出了十份 Lean 4 證明，方便研究者複核。

這項工作的關鍵不在於“模型獨立完成數學研究”的宣傳，而在於把候選推導、人工檢查和形式驗證組合成可重複流程。對研究團隊而言，模型可以快速探索大規模組合空間，Lean 則把最終結論約束在可檢查的證明內。短期適合用來尋找反例、生成證明草稿和篩選值得深入的方向；正式發表仍需要領域專家確認定義、假設與新穎性。未來評價這類係統時，應同時看證明是否通過形式化檢查、結果是否被同行接受，以及模型在不同問題上的穩定成本。

來源： - https://openai.com/index/ten-advances-in-mathematics - https://github.com/openai/ten-proofs - https://cdn.openai.com/pdf/ten-proofs-oai.pdf