Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids

TL;DR

This thesis in Lean 4 formalizes theorems in optimization, matroid theory, and grammars, emphasizing code readability, trustworthiness, and philosophical notions of beauty in mathematical formalization.

Contribution

It develops understandable, verifiable libraries in Lean 4 for diverse mathematical areas, integrating philosophical perspectives on beauty and truth into formal verification.

Findings

Formalized key theorems in optimization, matroids, and grammars.

Created readable and trustworthy Lean 4 libraries for mathematical theories.

Integrated philosophical insights into the formalization process.

Abstract

This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer Science). The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn't present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS (optimization theory, matroid theory, and the theory of grammars). In the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. In search for beauty, we focus on the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, most importantly, beauty is the means for shaping our place in the world and a source of redemption, where it can be viewed as a substitute for religion.