Per recordar les tàctiques que anirem aprenent, es pot consultar el resum de tàctiques com a referència.
També podeu veure el vídeo de la segona sessió del Bootcamp.
Aquest repositori és una introducció a la demostració de teoremes amb Lean.
Està basat en el repositori GlimpseOfLean de Patrick Massot.
L’objectiu és completar-lo en unes 4 hores.
Podeu treballar amb Lean mitjançant una de les 3 opcions següents: 1. Instal·lar Lean localment (la millor a llarg termini). 2. Utilitzar el servidor lean4web (per començar sense cap prerequisit). 3. Fer servir Codespaces o Gitpod (per no instal·lar res, però ens permet fer servir projectes més grans).
La manera més fàcil de provar Lean sense haver de crear cap tipus de compte és fer servir el servidor lean4web proveït pel Lean FRO. Podeu clicar els enllaços de més amunt.
Hi ha webs que ens permeten treballar més còmodament, però cal un compte a GitHub.
Per fer servir Codespaces, cliqueu al botó de sota estant
loggejat a GitHub. Escolliu l’opció 4-core i cliqueu
Create codespace. Després d’uns minuts apareixerà un editor
Lean en el propi navegador.
Gitpod s’assembla molt a Codespaces. Cliqueu el botó de sota,
premeu Continue i espereu uns minuts.
Per gaudir de l’experiència Lean completa, us caldrà instal·lar-lo en el vostre ordinador.
Per fer-ho, seguiu les instruccions oficials aquí.
La referència per aprendre Lean de veritat és el llibre Mathematics in Lean.