An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
William M. Farmer

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematical and Computational Methods · History and Theory of Mathematics
