计算机、证明和证据(英文)

有论者认为以电脑辅助进行之数学证明其实包含了经验性之前提,因此要接受此类证明,就得修改传统的"数学证明"的概念。本文审视此说法;以讨论Thomas Tymoczko的一篇关于四色定理得哲学意义的论文为发端,进而论及Tyler Burge等人的相关观点,并由此对上述说法提出质疑。

Computer,Proof,and Testimony

It has been claimed that computer-assisted proof utilizes empirical evidence in a manner unheard of in traditional mathematics and therefore its employment forces us to modify our conception of proof.This paper provides a critical survey of some arguments for this claim.It starts by revisiting a well known paper by Thomas Tymoczko on the computer proof of the Four-Color Theorem.Drawing on some ideas from the works of Tyler Burge and others,it then considers a way to see the philosophical significance of computer proof that casts doubts on the claim.