An Alternative Approach to Formal Mathematics that Focuses on
Communication and Accessibility

William M. Farmer

2026

Abstract

Formal mathematics is mathematics done within the framework of a
formal logic.  It offers major benefits to mathematicians as well as
to computing professionals, engineers, and scientists who use
mathematics in their work.  The standard approach to formal
mathematics, in which mathematics is done with the help of a proof
assistant and all details are formally proved and mechanically
checked, achieves these benefits and offers a very high level of
assurance that the results produced are correct.  However, since the
main goal of the standard approach is certification, the proof
assistants supporting the standard approach are generally complex,
based on unfamiliar logics, difficult to learn how to use, and far
removed from mathematical practice.  Thus the standard approach does
not adequately serve mathematics practitioners who are more interested
in communicating mathematical ideas than in formally certifying their
correctness or who prefer not to make the investment needed to gain
proficiency in the use of proof assistants.

This paper presents an alternative to the standard approach that
focuses on communication and accessibility, the two weaknesses of the
standard approach.  It is called the free approach to formal
mathematics since it is free of the obligation to formally prove and
mechanically check all details of a mathematical development.  The
paper argues that the free approach would serve the needs of the
average mathematics practitioner much better than the standard
approach.  It describes an implementation of the free approach based
on a logic named Alonzo, a practice-oriented version of Alonzo
Church's formulation of simple type theory.  And it calls for the
mathematics community to develop logics, software, and libraries of
formal mathematical knowledge to support the free approach and to
train mathematics practitioners to use them.