數學證明

**數學證明**，通常就噉簡稱**證明**，係數學家研究數學嘅工具，數學上嘅證明。喺數學證明嘅過程入面，數學家會先諗出一柞公理，即係一啲佢哋認為好明顯係真，唔使證明都可以攞嚟用嘅命題，或者係用一啲之前已經證明咗嘅命題（即係所謂嘅定理）。然後佢哋會靠住用呢啲公理同定理，再用一啲數學證明嘅方法推斷出一啲**實啱**嘅新命題，而呢啲新推出嚟嘅命題會俾好多數學家攞嚟詏，如果詏完一輪之後啲數學家覺得個證明冇問題嘅話，條新命題就會變成一條新嘅定理。呢啲新定理又有得攞去用嚟證明新啲嘅定理－於是乎數學知識就係噉增長。

如果一條命題要俾數學界接受係定理，佢就要有個令人滿意嘅證明，如果佢衹係有人覺得可能係啱但係冇俾人成功證明到嘅話，佢衹會係個猜想。

## 大分類
大體上，數學嘅證明有得分做兩種：

*非形式化嘅證明（Informal proof）－一種用自然語言－即係好似廣東話呢類日常傾偈用嘅語言－寫出嚟嘅論證，用嚟說服啲讀者某個定理或者論斷係啱。因為呢種證明用咗自然語言，而自然語言好多時冇數學語言噉精確，搞到非形式化嘅證明俾數學家覺得佢寬鬆得滯。非形式化嘅證明通常都係用喺應用嘅場合度，例如係科普講座、口頭辯論、或者初等教育－因為喺呢啲場合度啲讀者嘅水平冇噉高。

*形式化嘅證明（Formal proof）－一種唔係用自然語言，而係用數學語言寫出嚟嘅證明。數學語言係一連串既定嘅符號，每個符號都有一套標準化而且好明確嘅定義，令到啲數學家唔使憂個證明夠唔夠清楚明確。如果一個數學家係想向成個數學界證明某啲新定理或者理論嘅話，佢一定要用形式化嘅證明，先至可以說服到數學界佢個證明係夠精確嘅。

研究證明嘅形式同方法嘅理論喺學術上嗌做證明論。

## 常用嘅證明方法
### 直接證明

直接證明係指直接由啲大家都認為係唔使證明都可以當係啱嘅公理或者係之前俾人證明咗嘅定理嗰度出發，運用推理去推想證明嗰條定理出嚟，係最簡單直接嘅證明方法。基本上，個思路就係：

* 有若干數量嘅命題（P、Q...），因為佢哋係公理或者之前經已俾人證明咗，所以可以假設佢哋係啱嘅；
* 由呢柞命題度可以引申到一條新命題 R；
* 所以命題 R 都係啱嘅。

;例子
*要求*：證明「任何兩個雙數 x 同 y 加埋一齊，出嘅一定會係一個雙數」。

:如果一個數係雙數，噉佢一定會係 2 嘅倍數；（公理）
:設 x=2a，y=2b，而 a,b 係某啲整數；
:噉嘅話，\begin{matrix}x+y&=&2a+2b\\&=&2(a+b)\end{matrix}。
:2(a+b) 呢個數好明顯係 2 嘅倍數－噉佢一定係一個雙數，所以 x+y 係一個雙數。證明成功。

喺成個證明過程入面，個證明者淨係用咗一條公理，跟手就推咗條新定埋出嚟－係一個直接證明。

### 數學歸納法

數學歸納法專係用嚟證明一啲有良序性嘅定理。佢成個諗頭係在於要先證明以下兩樣嘢：

* 當 n=1 嘅時候，命題 P_n 係啱嘅；
* 當命題 P_k 係啱嘅時候，可以引伸到 P_{k+1} 都係啱嘅；

假如以上兩點成立到嘅話，噉就有得話「當 n=2 嘅時候，P_n 呢個命題會係啱」，而「當 n=3 嘅時候，P_n 呢個命題都會係啱」，如此類推，命題 P_n 對應所有嘅自然數（平時用嚟數嘢嘅數字）都係啱嘅。

;例子
*要求*：證明「如果 x\neq0\in\Z 係非零整數，噉對應所有正整數 n\in\Z_{>0}，x^{2n} 係正數。」（想要證明嘅命題 P_n）

:基本步驟：如果 n=1，x^{2n}=x^2，噉 x^2 係正數。（當 n=1 嘅時候，P_n 呢個命題係啱嘅。）
:歸納假設：如果 n=k 係啱嘅話，即係 n=x^{2k} 係正數。
:推斷：如果 n=k+1，

\begin{align}
x^{2n} &= x^{2(k+1)}\\
&= x^{2k+2}\\
&= x^{2k}\cdot x^2
\end{align}

（當 P_k 呢個命題係啱嘅時候，可以引伸到 P_{k+1} 都係啱嘅。）

證明成功。

### 否定證明

否定證明係一種利用*換質換位*邏輯嚟去證明一啲定理嘅證明方法。「換質換位」指嘅簡單啲講係話「P \rightarrow Q」同「 \neg Q \rightarrow \neg P 」呢兩句嘢喺邏輯上係有關嘅：如果「P 暗示 Q」係啱嘅，噉如果 Q 唔係真，噉 P 都唔會係真。例如係以下呢個論證：

* 如果蘇格拉底係一個人，噉佢嘅壽命會係有限嘅；（P \rightarrow Q）
* 如果蘇格拉底嘅壽命係冇限嘅，噉佢一定唔係一個人。（ \neg Q \rightarrow \neg P ）

如果將 P 同 Q 換做某啲數學命題，噉呢種思考方式就有得攞嚟做數學證明。

;例子
*要求*：證明「有個整數 x，如果 x^2 係雙數，噉 x 都一定係雙數。」

假設 x 唔係雙數，噉佢就係個單數。

兩個單數乘埋一齊一定係出個單數，所以如果 x 係單數，x^2 都一定會係個單數。（P \rightarrow Q）

所以如果 x^2 唔係單數，噉 x 都唔會係個單數。（ \neg Q \rightarrow \neg P ）

個個數一係就係單數一係就係雙數。

所以如果 x^2 係雙數，噉 x 都會係個雙數。證明成功。

### 反證法

反證法係一種古老嘅證明方法，利用咗「如果呢條命題成立，會有個唔合理嘅結果，所以呢條命題冇可能係啱嘅」呢點嚟證明某啲命題係錯嘅。佢條思路係：

* 先假設想否定嘅命題 P 係啱嘅；
* 由命題 P 嗰度引申一個荒謬嘅結果出嚟；
* 噉就可以話命題 P 係錯嘅。

;例子
*要求*：證明「假設 n\in\Z 係一個單數，噉 n^2 唔會係一個雙數」。

:假設 n\in\Z 係一個單數，再假設 n^2 係一個雙數。
:即係對應某啲自然數 k\in\Z，n=2k+1。計吓

\begin{align}
n^2 &= (2k+1)^2\\
&= 4k^2+4k+1\\
\end{align}

好明顯得出個結果係 n^2 唔係一個雙數，條假設自相矛盾。（唔合理嘅結果）

所以，「如果 n\in\Z 係一個單數，n^2 可以係一個雙數」呢句嘢唔成立－假設 n\in\Z 係一個單數，噉 n^2 唔會係一個雙數。

### 構造法

構造法一般係用嚟證明一啲存在性定理（話某啲嘢存在嘅定理）－用呢個證明嗰陣，用嗰個人會諗出一件有得用數學描述嘅物件出嚟，列出佢有啲乜嘢特性，再證明一件有呢啲數學物性嘅物件係存在嘅。佢條思路係噉嘅：

* 揾到有一個情況下，命題 P 係啱嘅；
* 證明到「喺至少一個情況下，命題 P 係啱嘅」。

;例子
*要求*：證明「唔係所有單數都係質數」（即係話「喺至少一個個案入面，有個單數唔係質數」）。

重點就係要揾個唔係質數嘅單數出嚟。

9 係個好簡單嘅例子，佢符合單數嘅定義（唔可以俾 2 整除），但又唔係質數（佢係 1、3、同佢自己嘅倍數）。

即係話揾到有一個情況下，命題 P （有個單數唔係質數）係啱嘅，噉就證明咗「唔係所有單數都係質數」呢句命題。

### 分類證明

分類證明係一種用嚟證明啲淨係描述緊數量有限嘅個案度嘅定理嘅一種證明方法。佢嘅過程係要先列出所有個案，再顯示喺所有個案入面，條命題都係成立嘅。條思路如下：

* 想要證明嘅命題 P 淨係描述緊*數量有限*嘅個案；
* 將所有命題 P 描述嘅個案列嗮出嚟；
* 顯示喺所有個案入面，P 嘅預測都係成立嘅；
* 證明到 P 呢句命題係啱嘅。

;例子
*要求*：證明「任何整數 n\in\Z，n^2+3n+7 係一個單數。」

如果 n 係雙數，噉就有一個整數 k\in\Z 符合 n=2k。

\begin{align}
n^2+3n+7 &= (2k)^2+3(2k)+7\\
&= 4k^2+6k+7\\
&= 2(2k^2+3k+3)+1     
\end{align}

因此，n^2+3n+7 係一個單數。

如果 n 係單數，噉就有一個整數 k\in\Z 符合 n=2k+1。

\begin{align}
n^2+3n+7 &= (2k+1)^2+3(2k+1)+7\\
&= 4k^2+10k+11\\
&= 2(2k^2+5k+5)+1     
\end{align}

因此，n^2+3n+7 係一個單數。

因為整數一係單數一係雙數，而喺以上兩個個案入面 n^2+3n+7 都係一個單數，所以「任何整數 n\in\Z，n^2+3n+7 係一個單數。」呢句命題成立。

## 相關概念

### 無字證明

* 無字證明，又有叫*無言證明*、*視覺證明*，係指用圖像呢啲直接用眼睇嘅方法嚟到嘗試證明一啲數學定理。呢種「證明」方法好多時會因為條線畫得唔夠直等嘅技術性原因而出錯，所以喺正式嘅數學研究嗰度好少可會有學者接納。

### 證明結尾

* 有陣時喺一個證明嘅結尾嗰度會寫咗 Q.E.D. 呢三個羅馬字母喺度，呢個係拉丁話 Quod Erat Demonstrandum 嘅縮寫，意思係「本嚟要證明嘅嘢」噉解。
* 廿一世紀嘅證明完畢符號通常係用  （實心黑色四方形）。佢個名叫墓碑，又或者叫*哈爾莫斯符號*－因為美國數學家 Paul Halmos 係第一個用呢種做法嘅。個墓碑有時係空心嘅「」。有啲人習慣證明引理嗰陣用空心墓碑，證明成個定理嗰陣先用實心墓碑。
* 仲有另外簡單嘅方法係寫 **proven** 或者**證畢**之類嘅文字。

### 證明唔到嘅嘢
* 有陣時有啲命題係證明唔到嘅，冇方法可以證明佢係真，又冇方法可以證明佢係假，呢啲命題係所謂嘅*決定唔到*嘅命題。歐幾里得幾何入面嘅平行公設就係一個例子。
* 哥德爾不完備定理表示咗，喺數學家會有興趣嘅命題當中至少有一啲係證明唔到嘅。

### 實驗數學

* 有一啲早期嘅數學家係唔靠證明嘅，但係由幾何學之父歐幾里德（公元前 300 年生）開始，數學證明就一路都係數學發展嘅基礎，直到 19 至 20 世紀都仲係噉。但係自從喺 1960 年代起，電腦嘅運算能力就開始變到愈嚟愈勁，所以開始有數學家研究數學嘢可唔可以用證明以外嘅方法研究－形成咗實驗數學呢個領域。

## 電腦輔助證明

直至廿世紀為止，學界一般都仲係覺得原則上任何嘅數學證明都可以由能力夠高嘅數學家嚟幫手肯定佢嘅有效性，但係家吓數學界成日都會用電腦輔助證明－即係用電腦幫手證明一啲定理，又或者用電腦做一啲長得滯搞到用人手計唔到嘅運算，例如四色定理嘅第一個證明就係由電腦輔助做嘅。初頭有唔少數學家擔心用電腦幫手會搞到啲證明有可能出錯，質疑電腦輔助證明嘅有效性。現時嘅數學家會用好多方法令到電腦輔助證明令人更加有信心，好似係重複噉檢查同埋用多個唔同程式做證明呀噉，而事實係，就算用人手做數學證明都係有可能出錯嘅。所以喺廿一世紀，數學界一般都唔抗拒用電腦幫手做數學證明。

## 睇埋
* 證明論
* 模型論
* 自動定理證明
* 無效證明
* 電腦輔助證明

## 引用

## 參考

* Alibert, D., & Thomas, M. (2002). *Research on mathematical proof. In Advanced mathematical thinking* (pp. 215-230). Springer Netherlands.
*.
*.
* Hanna, G., & Jahnke, H. N. (1996). *Proof and proving. In International handbook of mathematics education* (pp. 877-908). Springer Netherlands.
* Hardy, G. H. (1929). Mathematical proof. *Mind*, 38(149), 1-25.
*.
*.
*.