到2027年，我們不會接近於正式化在威爾斯證明費馬最後定理之前所使用和看起來的數學的幾個百分比。 到2035年，我們也不會有AI進行新穎和實際的數學研究（大多數的厄爾多斯和國際數學奧林匹亞問題集與此完全不同），而不涉及整個重點和難度（即弄清楚什麼實際上重要並且真正具有創造性）——這只會加速人類僅僅關心的部分（正式部分）。數學研究同樣關於確定正確的問題是什麼，什麼是有趣的與微不足道的，也許最重要的是對於結果為什麼重要的實際理解（!!!）比其他任何事情都重要。 這也沒有提到並非所有數學領域都有相同的計算“可訪問性”。 我們仍然非常遙遠（但我們更接近了！）於研究，特別是數學研究，能夠被AI“主導”，任何告訴你相反的人，要麼是以“極其無聊的研究定義”來理解，要麼是在撒謊，或者是個白癡，或者三者皆是。 我認為到2027年一半的新數學結果是AI生成的這個想法是可笑的，除非我們在某種程度上精神失常到將數學結果定義為僅僅是一些正式的符號串和基於一些簡單規則的邏輯推理。 明確來說，我的觀點並不是說數學的“自動形式化”不有效，它因為許多原因而非常有價值——主要是因為人類會做更好的數學，或者更好地利用他們的時間，但無疑它本身沒有價值，因此不會“自動化數學研究”。我的觀點也不是說AI永遠無法進行實際的數學研究：我相信它可以，但無疑它不會在兩年內從當前的2020-2025技術中掉出來。

真正的數學高手可能會站出來反對，我不是一個真正的數學高手，但我懷疑純粹的電腦怪人或純粹的數學怪人會有太多的反對意見，因為他們根本對兩邊的知識都不夠了解。

為了澄清，我認為我們目前正處於人工智慧能夠與人類結合提供新穎證明的時代，自動形式化將持續增長，而 GDM 可能很快就會獲得 Navier-Stokes 等等。 我的觀點不是說這沒有用，而是說根本上最困難的部分仍然是並且將仍然是由人類驅動，直到人工智慧研究有顯著進展（在我們目前的解碼器自回歸熱潮之上，而這種熱潮在未來幾年仍將持續）。

@nasqret 我特別將我的觀點縮小到「當前技術堆疊」，即自回歸解碼器專用的變壓器 + 10000 個粘合或固定的東西，據我所知，沒有任何真正的創新會在 2027 年（或 2030 年）之前被商品化，使這一切成為可能。