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/
-
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.