數(shù)學(xué)證明從簡單自明的公理/公設(shè)(選擇公里或許不在此列) + 已經(jīng)得到證明的定理，針對(duì)定義明確的對(duì)象，通過推理規(guī)則，得到需要的結(jié)論。

在推理規(guī)則中，有兩種類型，①邏輯規(guī)則，如前提/結(jié)論引入規(guī)則、置換規(guī)則、三段論等，這具有普遍有效性。②確定的數(shù)學(xué)規(guī)則，一是特定的數(shù)學(xué)運(yùn)算法則，有環(huán)境條件限制的，一般不具備普適性。如一個(gè)非阿貝爾群中卻讓群成員的乘法滿足了可交換性，肯定就是錯(cuò)誤的。如 {實(shí)數(shù)矩陣,矩陣乘法} 構(gòu)成的群其乘法不滿足交換律（小學(xué)就學(xué)過的幾個(gè)基本運(yùn)算規(guī)則??）。二是某些規(guī)定，如“關(guān)系R”，R可以是自反的,xRx。也可以是反自反的。

在驗(yàn)證舒爾茨證明過程中，①需要查看證明中引入的結(jié)果是否可靠（是否滿足mathlib中的定義，證明當(dāng)前命題需要引入的定理在當(dāng)前數(shù)學(xué)體系中是沒有的，機(jī)器要發(fā)現(xiàn)并進(jìn)行證明，這樣就可以作為前提引入到證明中了）。②使用的邏輯規(guī)則是否正確，使用的數(shù)學(xué)推理規(guī)則是否符合當(dāng)前的環(huán)境，問題是否和當(dāng)前的定義匹配?；蛟S這是Lean機(jī)器檢查證明過程是否正確的方法吧。一個(gè)一個(gè)步驟進(jìn)行檢查，如果都合規(guī)就證明是正確的。
計(jì)算機(jī)輔助證明，過去是把無限的可能性有限化后進(jìn)行一個(gè)一個(gè)證明，化整為零，暴力求解，如著名的四色定理。現(xiàn)在， Lean 則是從 1. 檢查可能存在的推理過程錯(cuò)誤 2.推理過程中需要引入前提有沒有，是否正確這個(gè)角度來進(jìn)行工作了，實(shí)在是讓人感慨。

https://mp.weixin.qq.com/s/79js4v0_teVuRa_2iu2Itg
數(shù)學(xué)家喜迎“大統(tǒng)一”理論的計(jì)算機(jī)輔助證明