William Farmer: An Alternative Approach to Formal Mathematics

An Alternative Approach to Formal Mathematics that Prioritizes Communication over Certification
Formal mathematics is mathematics done within a formal logic. It offers mathematics practitioners several major benefits over traditional mathematics. The standard approach to formal mathematics emphasizes certification: Mathematics is done with the help of a proof assistant and all details are formally proved and mechanically checked. Although there is a very good argument that the standard approach has been a big success, it has had very little impact on mathematical practice. Only a small slice of the millions of mathematics practitioners have ever used a formal logic or proof assistant in their work! We propose an alternative, communication-oriented approach to formal mathematics that is characterized by (1) the underlying logic is designed to be as close to mathematical practice as possible, (2) proofs are written in a traditional (nonformal) style, (3) mathematical knowledge is organized using the little theories method, and (4) supporting software is unencumbered by the machinery needed to develop and certify formal proofs. We believe that formal mathematics can be made more useful, accessible, and natural to a wider range of mathematics practitioners by implementing this alternative approach. We have begun an implementation of this approach based on a version of Church's type theory called Alonzo that admits undefined expressions, tuples, and subtypes. Alonzo is presented in the textbook W. M. Farmer, Simple Type Theory: A Practical Logic for Expressing and Reasoning About Mathematical Ideas, Birkhaeuser/Springer, 2023.