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

TL;DR

This paper proposes a new, accessible approach to formal mathematics called the free approach, emphasizing communication over formal certification, supported by a logic named Alonzo, to better serve practicing mathematicians.

Contribution

It introduces the free approach to formal mathematics, contrasting with the standard proof-assistant-based method, and presents an implementation using the Alonzo logic to enhance accessibility and communication.

Findings

The free approach prioritizes communication over formal proof certification.

Implementation of the free approach using the Alonzo logic.

Call for community development of tools and resources for the free approach.

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.