Simone, Marco (2026) Formalizing Mathematics in Lean. Bachelor's Thesis, Mathematics.
|
Text
FormalizingMathematicsinLean.pdf.pdf Download (533kB) | Preview |
Abstract
This thesis describes the formalization in the Lean 4 proof assistant, and on top of the Mathlib library, of the central results of the paper The quasi-Weierstraß form for regular matrix pencils by Berger, Ilchmann and Trenn [3]. The paper studies regular matrix pencils A − E∂ and the associated differential-algebraic equation Ex˙ = Ax by means of the Wong sequences, two sequences of nested subspaces whose limits V ∗ and W∗ decompose Kn into a direct sum; bases of these subspaces transform the pencil into the quasi-Weierstraß form, which separates the differential part of the equation from the algebraic one. The formalization covers the paper up to and including its main existence theorem (Theorem 2.6): the Wong sequences and their elementary properties, their termination in finite dimension, the image and kernel characterization of Lemma 2.3, the structure of V ∗ and W∗ (Proposition 2.4), and the existence of the quasi-Weierstraß form. Besides presenting the mathematics and the corresponding Lean development, the thesis discusses the process of formalization itself: the translation of the paper’s definitions into formal ones, the choices of representation that this requires, and the difficulties encountered. Particular attention is given to the proof of Theorem 2.6, whose first paragraph as published contains an error, later corrected in print after being observed by Fabian Wirth [4]. The formalization follows the corrected argument and makes explicit why the original step cannot be carried out: the proof assistant rejects it, because the missing implication is false. This episode illustrates in a concrete case the principal benefit of machine-checked mathematics, namely that a missing step of a proof, however plausible in appearance, is not accepted without justification.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Trenn, S. and Seri, M. |
| Degree programme: | Mathematics |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 28 Jul 2026 06:32 |
| Last Modified: | 28 Jul 2026 06:32 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/37461 |
Actions (login required)
 |
View Item |