Taller de LEAN

El demostrador de teoremes LEAN és un assistent de demostració desenvolupat per Leonardo de Moura a Microsoft Research. https://leanprover.github.io/

Per a instal·lar LEAN seguiu les instruccions https://leanprover-community.github.io/

Material de suport

• J. Avigad, K. Buzzard, R.Y. Lewis, P. Massot | Mathematics in Lean.

• J.A. Alonso | Matemáticas con Lean.

• J.A. Alonso | Lógica con Lean.

• J. Blanchette, J. Limperg, V.Nummelin| Logical verification 20/21

• A. Baanen, A. Bentkamp, J. Blanchette, J. Hölzl, J.Limperg | The Hitchhiker’s Guide to Logical Verification.

• Imperial College London | Formalising Mathematics.