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.
万方数据
维普
