{"id":"arxiv/2602.12891","url":"https://arxiv.org/abs/2602.12891","tags":["cs.LO","math.HO"],"score":0,"title":"Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids","domain":"cs.LO","source":"arxiv","authors":["Martin Dvorak"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-13","reactions":{}}