An Alternative Approach to Formal Mathematics - Prioritizing Communication over Certification

Explore an alternative approach to formal mathematics that prioritizes communication over certification in this 34-minute lecture by William Farmer at the Hausdorff Center for Mathematics. Delve into the limitations of the standard approach to formal mathematics, which emphasizes certification and proof assistants but has had minimal impact on mathematical practice. Discover a communication-oriented approach characterized by four key elements: a logic designed to closely mirror mathematical practice, proofs written in traditional non-formal style, organization of mathematical knowledge using the little theories method, and software unburdened by formal proof certification machinery. Learn about the implementation of this approach based on Alonzo, a version of Church's type theory that accommodates undefined expressions, tuples, and subtypes. Gain insights into how this alternative approach aims to make formal mathematics more accessible, useful, and natural for a broader range of mathematics practitioners.