Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids
Martin Dvorak
cs.LO
Feb 13, 2026 · v1
TL;DR
Thesis develops Lean 4 libraries formalizing optimization theory, matroid theory, and the theory of grammars.
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.
Problem
Formal verification of mathematical theorems across diverse areas (optimization, matroids, grammars) in a unified framework that prioritizes readability and correctness of definitions over ease of proof manipulation.
Approach
The thesis develops Lean 4 libraries presenting definitions and results from optimization theory, matroid theory, and the theory of grammars. The emphasis is on readable and believable definitions (choosing faithful representations over easier-to-work-with ones) and on identifying the trusted code in each project. The philosophical framework of Roger Scruton on beauty guides the presentation.
Results
Three formalized areas are completed in Lean 4: optimization theory, matroid theory, and the theory of grammars. The code is designed to stand for itself without external documentation, with definitions chosen for readability and faithfulness to mathematical intent.
