数学证明是一种演绎论证，用来表明某个数学命题必然成立。它从公理、定义和已证明的定理出发，逐步推进，每一步都依据逻辑规则由前面的步骤推出。经验证据或归纳推理只能使一个论断显得可信，而一个有效的证明则表明，该论断在其假设所涵盖的一切情形下都成立。正因如此，证明处于数学的核心地位。有论述将证明描述为一串“以严格的逻辑规则”相连的命题，并指出正是由于这一点，数学家可以像信赖当今的成果一样，放心地使用欧几里得在2300年前完成的数学工作。
起源
数学活动的历史远比演绎证明悠久。古埃及和美索不达米亚早已有计算与测量的实践。不过，许多学者认为，真正意义上的数学诞生于公元前6世纪前后的古希腊，因为演绎证明正是在那时首次出现。亚里士多德认为，米利都的泰勒斯认识到，重要的不仅是我们知道什么，还有我们如何知道，并在演绎方法中为知识找到了根据。此后数百年间，希腊数学家证明了某些量是无理数，并发展出穷竭法。后来，阿基米德运用这一方法求出了面积和体积。
约公元前300年，欧几里得在其著作《几何原本》中将几何学的演绎方法系统化。该书先列出定义、公设和公理，再由此依次推导出各个命题，其中著名的例子包括勾股定理的证明，以及素数有无穷多个的证明。千百年来，欧几里得的公理化风格一直被奉为严格论证的典范，影响不仅限于数学，也延及哲学和自然科学。其他数学传统同样为其结果提供论证：中国、印度和伊斯兰世界的数学家都曾为自己的算法和恒等式给出论证，只是形式往往有别于希腊的公理化模式。
证明方法
数学中常见的论证模式有以下几种：
- 直接证明：从假设出发，通过一连串蕴涵关系推出结论。
- 逆否证明：要证明“若P则Q”，只需证明“非Q”蕴涵“非P”。
- 反证法：假设命题不成立，进而推出逻辑矛盾。证明√2是无理数的经典方法就是如此。
- 数学归纳法：先证明命题对第一个自然数成立，再证明若它对任意n成立，则对n + 1也成立。两步合起来，即可证明命题对所有自然数成立。
- 构造性证明与非构造性证明：构造性证明会给出所断言存在之对象的具体实例；非构造性证明只表明该对象必然存在，却不把它构造出来。非构造性证明有时会引起争议。例如，大卫·希尔伯特在不变量理论中的一项代表性成果，就是以非构造性的方式、本质上借助反证法证明的，这在当时颇具争议。
- 穷举证明：把问题分成有限多种情形，逐一加以验证。
- 反例：只需一个反例，就足以说明一个全称论断是错误的。
实际发表的证明通常用自然语言夹杂符号写成，并略去专家能够自行补全的常规步骤。一个证明能否被接受，在一定程度上是一个社会过程：其他数学家会通过同行评审和进一步讨论来阅读、检验其论证。
严格性与数学基础
17、18世纪，微积分迅速发展，但其中有关无穷小的论证往往依赖直觉。19世纪，柯西、魏尔斯特拉斯等人以极限和连续性的精确定义为基础，重建了数学分析。非欧几何的发现也表明，公理最好被视为假定，而非不证自明的真理。
1900年前后，数学家试图为整个数学奠定稳固的逻辑基础，主要工具包括集合论、符号逻辑以及皮亚诺公理等公理系统。到20世纪初，他们确定了所要采用的公理，还引入了各种逻辑系统和标准，力图使论证进一步“形式化”。在这一框架下，形式证明是一个有限的公式序列，其中每个公式要么是公理，要么依据固定的推理规则由前面的公式推出。希尔伯特希望证明这类系统是一致的，而哥德尔不完备定理（1931年）表明这一愿望存在局限：任何足以表达算术的一致形式系统，都包含它无法证明的真命题，并且无法证明自身的一致性。
计算机辅助证明
计算机改变了证明的发现方式，也改变了证明的检验方式。1976年，四色定理成为第一个借助计算机程序验证的重要定理，其证明依赖机器检查数量极其庞大的情形。这引发了哲学上的疑问：有批评者认为，这类证明包含的逻辑步骤太多，人类实际上无法核验。
另一个例子是关于球体堆积的开普勒猜想，最早由约翰内斯·开普勒于1611年提出。1998年，托马斯·黑尔斯宣布了一个高度依赖计算机的证明，审稿人表示对其正确性有“99%的把握”。为此，黑尔斯发起了Flyspeck项目，对该证明进行形式化验证。项目于2014年8月10日正式完成，综合使用了Isabelle和HOL Light两种证明助手。
证明助手自20世纪60年代起逐步发展。使用证明助手时，用户须以机器可读的语言写出每一个定义和证明的每一步，再由软件检查其逻辑。常用的证明助手有Coq、Isabelle和Lean等。Lean的社区库Mathlib发展迅速，到2026年初已收录12万多个定义和约25万条经过验证的定理。形式化还能发现经典文献中的错误：2024年，有人用Lean对欧几里得《几何原本》第一卷进行形式化，发现了欧几里得证明中的错误。
证明与人工智能
自动定理证明可以追溯到计算机科学发展的早期，近年来的进展则来自它与机器学习的结合。在2024年国际数学奥林匹克竞赛中，谷歌DeepMind的AlphaProof与AlphaGeometry 2联合取得的成绩，仅比人类选手的金牌分数线低一分。AlphaProof用形式语言Lean生成证明，这种形式化方法的主要优势在于能够保证正确性。
2025年，基于大语言模型的系统用自然语言写出了竞赛证明。谷歌DeepMind的Gemini Deep Think所给出的解答经官方评分并认证为35/42分，达到金牌标准。OpenAI也报告其系统取得了相同分数，但这一成绩来自其自行组织的评估，由往届奖牌得主评分，而非经IMO协调员认证。AI系统给出的自然语言证明仍需人工核查，而它们的出现也再度激发了人们将人工智能与形式化验证相结合的兴趣。
参考来源
- The History and Concept of Mathematical Proof Steven G. Krantz1math.wustl.edu
- 1. Introduction — Logic and Proof 3.18.4 documentationleanprover-community.github.io
- In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?quantamagazine.org
- Computer-assisted proofen.wikipedia.org
- Kepler conjectureen.wikipedia.org
- Kepler Conjecture -- from Wolfram MathWorldmathworld.wolfram.com
- Autoformalizing Euclidean Geometryarxiv.org
- GitHub - loganrjmurphy/LeanEuclid: LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean. · GitHubgithub.com
- An Open Recipe for IMO Gold: Training Nemotron for Olympiad Mathematicsarxiv.org
- Winning Gold at IMO 2025 with a Model-Agnostic ...arxiv.org
- AI Reasoning: Gold-Medal Performance at the 2025 IMOintuitionlabs.ai