作为数学革命的形式化证明  

Formal Proof as a Mathematical Revolution

作　　者：杨帆 YANG Fan(College of Public Administration and Humanities,Dalian Maritime University,Dalian 116026,China)

机构地区：[1]大连海事大学公共管理与人文艺术学院,大连116026

出　　处：《自然辩证法研究》2024年第1期107-112,共6页Studies in Dialectics of Nature

基　　金：中央高校基本科研业务费专项资金资助“面向机器定理证明的模糊逻辑研究”(3132022308)。

摘　　要：随着计算机科学的兴起,数学家可以通过计算机完成对数学定理的证明与验证,由此形成了形式化证明的相关领域。在形式化证明的助力下,诸多数学难题得以攻破,这无疑改变了传统数学实践的范式。然而,学界对于形式化证明所引发的认识论转向的论述尚不充分,究其原因主要有两个方面:其一是缺乏对形式化证明的本体论考察,其二是对数学革命的定义存在分歧。对形式化证明中人脑证明和机器证明进行区分,同时厘清两种不同的革命定义,可以为形式化证明作为数学革命的观点提供辩护。With the rise of computer science,mathematicians can accompolish the proof and verification of mathematical theorems via computers,thus leading to the field of formal proof.With the help of formal proof,many mathematical problems have been solved,which undoubtedly changed the para-digm of traditional mathematical practice.However,the epistemological turn motivated by formal proof has not yet been adequately discussed in the aca-demic community.This is mainly due to two reasons:one is the lack of ontological investigation on formal proof,the other is the disagreement on the defi-nition of revolution.Distinguishing between human brain proof and machine proof in formal proof,and clarifying two different definitions of revolution,can provide a defense for the view of formal proof as a mathematical revolution.

关 键 词：形式化证明 机器定理证明 数学革命 

分 类 号：N031[自然科学总论—科学技术哲学]