Formal Mathematics for the Masses

William M. Farmer

2021

Abstract

The campaign to transform traditional mathematical practice into a
formal discipline appears to have been a great success.  Several
sophisticated proof assistants have been developed, a great deal of
mathematical knowledge has been formalized, a growing number of
researchers in computing and mathematics are now using proof
assistants to check the theorems they prove, and a new area of
computing called formal methods has been established in which formal
mathematics is used in the development of hardware and software.
However, the campaign has largely been a failure when viewed from a
broader perspective.  It has had almost no impact on mathematical
practice.  Far less than 1% of all mathematics practitioners have ever
used a formal logic or a proof assistant in their work.  We propose an
alternative approach to formal mathematics that is characterized by
(1) proofs are written in a traditional (nonformal) style, (2) the
underlying logic is as close to mathematical practice as possible, (3)
mathematics is organized in accordance with the little theories method
as a theory graph, and (4) supporting software systems are easy to
build and use.  We have begun a research program called Formal
Mathematics for the Masses to make formal mathematics more useful,
accessible, and natural to a wider range of mathematics practitioners
by implementing this alternative approach.