一位無名碩士生聲稱證明 zeta(5) 為無理數的預印本，已在 FrontierMath 基準測試中被標記為已解決。此驗證是透過自動化的 Lean 形式化完成，確認了證明的有效性。 這很重要，因為它展示了 AI 驗證非專家所撰寫複雜數學證明的能力，挑戰了傳統的學術階層。這突顯了形式化驗證在確認數論中開放研究問題方面日益增長的角色。 作者 Aabir Fauzan 是一位沒有數學博士學位的碩士生，但他的證明使用了漢克爾行列式，並透過 Lean 進行了形式化。該結果解決了關於黎曼 Zeta 函數奇數值無理性這一長期存在的開放問題。
事件背景
阿培里常數 zeta(3) 由羅傑·阿培里於 1978 年證明為無理數，但其他奇數值如 zeta(5) 的無理性在數十年間仍未得到證明。FrontierMath 是由 Epoch AI 建立的基準測試，用於測試 AI 系統解決具有挑戰性且此前未經檢驗的數學問題的能力。Lean 是一種證明輔助工具，用於將數學證明形式化，確保其邏輯嚴謹且可由機器驗證。
社群觀察
社區成員對作者的背景感到驚訝，指出他是一位無名的數學碩士生，並非數學博士。大家對使用 Lean 進行自動驗證感到興奮，儘管有些討論提到了早期嘗試以及類似證明中的邏輯缺陷。
