HIIT Foundations Friday: Niklas Halonen
HIIT Foundations Friday is a monthly get-together event for the community typically consisting of a tutorial and lunch as well as follow-up activity and discussions. This activity is part of the HIIT focus area on Foundations of Computing. On this page, you will find a brief overview of each talk, past and future as well as information about our current venue.
When
–
Where
Onsite
Siltavuorenpenger 3 A, Athena, Room 169
Niklas Halonen (Aalto University): Computer Formalization of the Real Numbers in Lean 4
I will introduce a construction of the (Cauchy) reals using quotient types in the Lean 4 theorem prover, as well as formalization tools like linarith, ring, the simplifier simp, its augmentation, and metaprogramming with custom tactics. The approach is based on Riccardo Brasca's (Real) Numbers game. For an in-depth documentation about Lean's quotient types, see: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/ and https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/