Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids
M. Dvorak, Pursuit of Truth and Beauty in Lean 4f: Formally Verified Theory of Grammars, Optimization, Matroids, Institute of Science and Technology Austria, 2026.