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.

翻译：本论文通过定理的形式化验证，记录了一段追求真理与美的旅程。为此，我们在Lean 4中开发了库，呈现了来自数学与计算机科学（MathematiCS）多个领域的定义与结果。其目标是创建可理解、可信、有用且优雅的代码。代码应尽可能独立自明，无需额外文档；然而，本文仍冗余地记录了我们的代码成果，并提供了代码中未包含的额外背景。本论文面向了解Lean 4但不熟悉所涉及主题的读者。我们在数学与计算机科学的三个形式化领域（优化理论、拟阵理论和语法理论）中展现了真理与美。在追求真理方面，我们专注于识别每个项目中的可信代码并忠实地呈现它们。我们强调定义的可读性与可信性，而非选择更易于操作的定义。在探寻美的过程中，我们聚焦于罗杰·斯克鲁顿的哲学框架，他强调美不仅仅是装饰，更重要的是，美是塑造我们在世界中位置的手段，也是救赎的源泉，在此意义上可被视为宗教的替代品。