氛圍證明的時代已經來臨。 來自 @HarmonicMath 的亞里士多德被用來在 @leanprover 中形式化陶哲軒對厄爾多斯問題的證明。 我們開始看到 AI 在新的數學發現中顯著貢獻。當與形式驗證結合時，我們將不再需要人類來審查和檢查證明的有效性，這將使飛輪轉動得更快，並大大加速前沿的進展。