This report examines the transition in mathematical verification from traditional constructive proofs to non-constructive logic and the contemporary integration of artificial intelligence in formalizing complex theorems.

本報告探討了數學驗證從傳統構造性證明向非構造性邏輯的轉型，以及當代如何將人工智慧整合於複雜定理的形式化過程中。

The historical trajectory of mathematical proof underwent a significant shift in the 19th century with the emergence of non-constructive proofs. Unlike constructive methods, which require the explicit exhibition of a mathematical object, non-constructive proofs establish existence through logical contradiction. A primary example is the 'pigeonhole principle,' which asserts a shared attribute within a set without identifying the specific subjects. David Hilbert championed this approach, notably in 1888 when he demonstrated the existence of finite generating sets for invariants without specifying their composition. This methodology relied upon the 'law of the excluded middle,' a logical axiom stating that a proposition is either true or its negation is true.

數學證明的歷史軌跡在 19 世紀隨著非構造性證明的出現而發生重大轉向。與需要明確展示數學對象的構造性方法不同，非構造性證明透過邏輯矛盾來確立存在性。一個主要例子是「鴿巢原理」，它主張一個集合中存在共同屬性，而無需識別具體對象。大衛·希爾伯特支持這種方法，尤其是在 1888 年，他證明了不變量具有有限生成集，而未指定其組成。此方法依賴於「排中律」，即一個邏輯公理，主張一個命題要麼為真，要麼其否定為真。

This shift precipitated a philosophical schism between Hilbert's formalism—which viewed mathematics as the manipulation of symbols—and L.E.J. Brouwer's intuitionism. Brouwer contended that mathematical objects must be mentally constructible to be valid, thereby rejecting the application of the law of the excluded middle to infinite sets. This intellectual conflict manifested institutionally within the journal Mathematische Annalen, culminating in the 1928 dismissal of the editorial board by Hilbert. While Hilbert's approach became the prevailing standard, Kurt Gödel later challenged formalism via his incompleteness theorem, suggesting that symbolic manipulation cannot achieve total consistency.

這一轉向導致了希爾伯特的形式主義（將數學視為符號操作）與 L.E.J. 布勞威爾的直覺主義之間的哲學分歧。布勞威爾主張數學對象必須在心智上可構造才有效，因此拒絕將排中律應用於無限集。這場知識衝突體現於期刊《數學年誌》中，最終導致希爾伯特在 1928 年解散編輯委員會。雖然希爾伯特的方法成為了主流標準，但庫爾特·哥德爾隨後透過其不完備定理挑戰了形式主義，指出符號操作無法實現完全的一致性。

In the contemporary era, the focus has shifted toward the formalization of mathematics through computational languages such as Lean. Kevin Buzzard of Imperial College London is currently leading an initiative to formalize Andrew Wiles's 1993 proof of Fermat's Last Theorem. This process involves translating human-readable proofs into machine-verifiable code, contributing to the Mathlib repository. The integration of Large Language Models (LLMs) has accelerated this process; for instance, a recent workshop saw the volume of project code double in a single day. However, the use of AI introduces a dichotomy between 'efficient' human-authored code and 'verbose' AI-generated code, the latter of which some researchers characterize as 'slop' due to its potential for instability during software updates.

在當代，焦點已轉向透過 Lean 等計算語言將數學形式化。倫敦帝國學院的 Kevin Buzzard 目前正領導一項計劃，將安德魯·懷爾斯 1993 年關於費馬最後定理的證明形式化。此過程涉及將人類可讀的證明翻譯成機器可驗證的代碼，並貢獻至 Mathlib 儲存庫。大型語言模型 (LLM) 的整合加速了這一過程；例如，最近的一場工作坊見證了項目代碼量在單日內翻倍。然而，AI 的使用在「高效」的人類編寫代碼與「冗長」的 AI 生成代碼之間產生了對立，後者被部分研究人員稱為「廢料」(slop)，因其在軟體更新時具有潛在的不穩定性。

Mathematics is currently transitioning toward an industrialization of the intellectual process, where AI-driven formalization may eventually produce logically valid proofs that exceed human cognitive comprehension.

數學目前正轉向知識過程的工業化，AI 驅動的形式化最終可能會產生邏輯有效但超出人類認知理解能力的證明。