Formalization

Lean Bootcamp

Materials can be found at here. A recording of the second session is available as well:

The geometry game

A Lean Game to learn Hilbert geometry and formalization. You can also try the older (and deprecated) Lean 3 game.

Formalització a la secundària

Talk "Ensenyant formalització a través de LEAN" (in Catalan).