摘　要：在信息化时代，人们能够使用计算机实现对数学定理的形式化证明，由此改变了数学实践的范式。鉴于形式化证明中涉及到人脑证明、机器证明和数学形式三种不同类别的存在，有必要从本体论层面对其进行考察。彭罗斯的三个世界理论发展自波普尔，并以其将数学形式作为柏拉图世界的独立存在而适用于形式化证明的本体论构建。为了使彭罗斯的三个世界理论能够作为形式化证明的本体论，还需要对其理论中世界间的关系进行改造。改造后的形式化证明的本体论为“数学是发现还是发明”这一著名问题提供了进一步的反思，彰显出三个世界理论带来的崭新视角。

关键词：形式化证明 三个世界 本体论 数学哲学

摘　要：哈金提出的两种证明观念把握了数学证明的内在特性，并明确地建立起二者对立与互补的态势，从而使得两种证明观念间的张力得以显现。从数学史的视角来看，数学家们从未对证明观念达成完全一致，因此两种证明观念间的张力是数学哲学中不容忽视的议题。从哈金的论述出发，通过对数学史中若干案例的考察，可以将两种证明观念与数学实践中的形式化证明和非形式化证明进行对应，从而加深对两种证明观念及其间张力根源的理解。

关键词：数学证明 数学哲学 形式化证明 非形式化证明