Seminar on Formalized Mathematics
The seminar meets Fridays at 13:15–14:00 in room U3039 of the main building of University of Helsinki (Fabianinkatu 33).
Anyone interested in formalization of mathematics is welcome!
Upcoming talks
-
Lauri Oksanen (University of Helsinki)Autoformalizing regularization theory
A machine-checked proof certifies a formal statement, and the human task is to confirm that each formal statement says what was intended. This is a substantial amount of work in the case of linear regularization theory that we autoformalized recently. I will describe the organization of our library and some tools that make this task manageable.
Past talks
Past talks are listed in the archive.