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

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