TY - RPRT TI - Pursuit of Truth and Beauty in Lean 4: Formally Verified Theory of Grammars, Optimization, Matroids AU - Martin Dvorak PY - 2026 UR - https://arxiv.org/abs/2602.12891 ID - 2602.12891 ER -