数学证明从简单自明的公理/公设(选择公里或许不在此列) + 已经得到证明的定理，针对定义明确的对象，通过推理规则，得到需要的结论。
在推理规则中，有两种类型，①逻辑规则，如前提/结论引入规则、置换规则、三段论等，这具有普遍有效性。②确定的数学规则，一是特定的数学运算法则，有环境条件限制的，一般不具备普适性。如一个非阿贝尔群中却让群成员的乘法满足了可交换性，肯定就是错误的。如 {实数矩阵,矩阵乘法} 构成的群其乘法不满足交换律（小学就学过的几个基本运算规则😅）。二是某些规定，如“关系R”，R可以是自反的,xRx。也可以是反自反的。
在验证舒尔茨证明过程中，①需要查看证明中引入的结果是否可靠（是否满足mathlib中的定义，证明当前命题需要引入的定理在当前数学体系中是没有的，机器要发现并进行证明，这样就可以作为前提引入到证明中了）。②使用的逻辑规则是否正确，使用的数学推理规则是否符合当前的环境，问题是否和当前的定义匹配。或许这是Lean机器检查证明过程是否正确的方法吧。一个一个步骤进行检查，如果都合规就证明是正确的。
计算机辅助证明，过去是把无限的可能性有限化后进行一个一个证明，化整为零，暴力求解，如著名的四色定理。现在， Lean 则是从 1. 检查可能存在的推理过程错误 2.推理过程中需要引入前提有没有，是否正确这个角度来进行工作了，实在是让人感慨。
https://mp.weixin.qq.com/s/79js4v0_teVuRa_2iu2Itg
数学家喜迎“大统一”理论的计算机辅助证明
网友评论