This report examines how mathematical verification has changed over time, moving from traditional constructive proofs to non-constructive logic and the current use of artificial intelligence to verify complex theorems.

本報告探討數學驗證如何隨時間演變，從傳統的構造性證明轉向非構造性邏輯，以及目前利用人工智慧來驗證複雜定理的情況。

The way mathematicians prove theories changed significantly in the 19th century with the rise of non-constructive proofs. While constructive methods require a mathematician to show a specific example of a mathematical object, non-constructive proofs prove that something exists by showing that the opposite is impossible. For example, the 'pigeonhole principle' asserts that a shared characteristic exists within a group without identifying exactly who has it. David Hilbert promoted this approach, using the 'law of the excluded middle,' which states that a statement must be either true or false.

數學家證明理論的方式在 19 世紀隨著非構造性證明的興起而發生顯著變化。構造性方法要求數學家展示數學對象的具體範例，而非構造性證明則是透過證明相反情況是不可能的，來證明某樣東西存在。例如，「鴿巢原理」主張一個群體中存在共同特徵，而無需確定具體是誰擁有該特徵。大衛·希爾伯特推廣了這種方法，使用了「排中律」，即規定一個陳述必須不是真就是假。

This shift caused a major disagreement between Hilbert's formalism, which treated mathematics as a system of symbols, and L.E.J. Brouwer's intuitionism. Brouwer argued that mathematical objects must be mentally constructed to be valid; consequently, he rejected the law of the excluded middle for infinite sets. This conflict became so intense that it led to a professional split within the journal Mathematische Annalen in 1928. Although Hilbert's view became the standard, Kurt Gödel later challenged it by suggesting that symbolic systems cannot be completely consistent.

這種轉變導致希爾伯特將數學視為符號系統的形式主義，與 L.E.J. 布勞華的直覺主義之間產生重大分歧。布勞華主張數學對象必須經過心智構造才有效；因此，他拒絕將排中律應用於無限集。這場衝突如此激烈，以至於導致 1928 年學術期刊《Mathematische Annalen》內部發生專業分裂。儘管希爾伯特的觀點成為了標準，但庫爾特·哥德爾隨後挑戰了這一點，指出符號系統無法完全一致。

Today, the focus has moved toward using computer languages like Lean to formalize mathematics. For instance, Kevin Buzzard from Imperial College London is leading a project to translate Andrew Wiles's 1993 proof of Fermat's Last Theorem into machine-verifiable code. Furthermore, the use of Large Language Models (LLMs) has greatly increased the speed of this work. However, this introduces a new problem: while humans write efficient code, AI often produces 'verbose' or messy code, which some researchers call 'slop' because it can be unstable during software updates.

如今，焦點已轉向使用如 Lean 等電腦語言將數學形式化。例如，倫敦帝國學院的 Kevin Buzzard 正在領導一個項目，將 Andrew Wiles 在 1993 年對「費馬最後定理」的證明翻譯成機器可驗證的程式碼。此外，大型語言模型 (LLM) 的使用大大提高了這項工作的速度。然而，這也引入了一個新問題：人類編寫的程式碼高效，而 AI 經常產出「冗長」或混亂的程式碼，一些研究人員將其稱為「slop」，因為它在軟體更新期間可能會不穩定。

Mathematics is now moving toward a more industrial process. In the future, AI-driven formalization may create logically correct proofs that are too complex for humans to understand.

數學現在正走向一個更工業化的過程。未來，AI 驅動的形式化可能會創造出邏輯正確，但複雜到人類無法理解的證明。