| Abstract |
Interactive theorem provers (ITPs) are becoming crucial in mathematics, supporting the development of fully verified proofs and mathematically rigorous infrastructure.
Their importance comes not only from catching mistakes that humans overlook, but also from enabling large-scale formalization projects that would be impossible to manage manually.
In this talk, I will give an accessible overview of formalizing mathematics in Lean4 and outline how its underlying theory and tooling support modern proof development.
In advance, I will present several mathematical projects that showcase the strengths of ITPs. |
