A càrrec d’en Marc Masdeu (UAB)
L'assistent de demostracions LEAN és un llenguatge que ens permet escriure codi que conté definicions, enunciats i demostracions matemàtiques, i que no ens permet cometre errors. En els últims dos anys he estat utilitzant aquest sistema per introduir estudiants de diversos nivells al món de la formalització. Explicaré com ensenyem la geometria de Hilbert a estudiants de 4t d'ESO i Batxillerat fent servir aquest llenguatge, i com també l'hem fet servir amb estudiants de diferents cursos de matemàtiques a la UAB, sota el programa Lean a l'Aula. Veurem com s'interactua amb aquest sistema a la pràctica, i entre tots formalitzarem alguna demostració.
https://zonavideo.upc.edu/video/66308cf34f108c539f41c689