一种侧重于沟通与可及性的形式数学替代方法

形式数学是基于形式逻辑框架内完成的数学工作。它为数学家以及使用数学的计算专业人员、工程师和科学家带来诸多好处。标准的形式数学方法通过帮助证明助手，形式地完成所有细节的证明并进行机械检查，实现了这些好处，并确保所产出结果的正确性。然而，由于标准方法的主要目标是认证，支持标准方法的证明助手通常复杂，基于不熟悉的逻辑，学习使用困难，远离数学实践。因此，标准方法未能充分满足那些更关注沟通数学思想而非形式认证正确性，或不愿投入学习证明助手技能的平均数学从业者的需求。本文提出一种替代方法，侧重于沟通和可及性，这两种是标准方法的弱点。该方法称为自由形式数学方法，因为其无需形式地证明和机械检查数学发展中所有细节。本文论证自由方法能更好地满足平均数学从业者的需求。它描述了基于名为Alonzo的逻辑实现，该逻辑是阿隆佐· Church关于简单类型论表述的实用版本。我们呼吁数学社区发展支持自由方法的逻辑、软件和形式数学知识库，并培训数学从业者使用这些工具。