Taller de Lean 4

Lean for Mathematical Research and Teaching: Collaborative Workshop

Els professors J.Ll. Figueras i J. Puig organitzen un taller sobre Lean 4 i les seves aplicacions a la recerca i la docència matemàtica, que tindrà lloc entre el 27 de gener i el 17 de febrer de 2027, en el marc de les activitats de formació de l'ICE de la UPC.

Taller col·laboratiu de Lean per a la recerca i docència matemàtica

Lean és un llenguatge de programació i un assistent de demostració que permet formalitzar definicions, enunciats i demostracions matemàtiques i verificar-ne rigorosament la correcció. Juntament amb la biblioteca Mathlib, s'està convertint en una eina cada vegada més rellevant en la recerca matemàtica, especialment amb els avenços recents en intel·ligència artificial.

La proposta és organitzar un taller pràctic i col·laboratiu (working seminar) en què puguem aprendre a utilitzar Lean conjuntament. No pretenem fer un curs expositiu tradicional, sinó crear un espai on explorar l'eina, resoldre exercicis, compartir dificultats i discutir possibles aplicacions a la nostra recerca i docència.

Començarem des de zero, de manera que no cal tenir coneixements previs de Lean. També explorarem l'ús de models de llenguatge (LLMs) per ajudar en la formalització i verificació de demostracions.

Informació pràctica:

Dates: 27 de gener, 3, 10 i 17 de febrer de 2027.

Horari: de 14:00 a 16:00 (8 hores en total).

Format: primera sessió presencial a la FME i les tres següents en línia.

Destinataris: PDI de matemàtiques i àmbits afins.

Places: entre 4 i 20 participants.

Inscripcions: Podeu consultar el portal de formació de l'ICE de la UPC: https://formacio.ice.upc.edu/

Ens agradaria que aquesta activitat també servís per començar a crear una petita comunitat de persones interessades en Lean dins de la UPC i, si hi ha interès, donar-li continuïtat més endavant.

Si us interessa participar-hi, feu-ho saber als organitzadors!