Lean: un foro colaborativo ----------------------------
La idea es sencilla: formalizar todos los conocimientos matemáticos en un asistente de pruebas libre y abierto llamado Lean (****).
Lean es, por tanto, un programa que permite verificar demostraciones matemáticas. Este tipo de programas se ha utilizado para demostrar el teorema de los cuatro colores (véase los Grafos, Bibliothèque Tangente 54, 2015) o la conjetura de Kepler sobre el apilamiento de esferas (véase Tangente 158, 2014). Uno de los asistentes de pruebas más utilizados es Coq, desarrollado por Inria.
Lean está desarrollado por Microsoft Research en C++ (Leonardo de Moura, 2013). Actualmente lo utilizan, entre otros, Thomas Hales, quien demostró la conjetura de Kepler.
Para ello, los usuarios se reúnen en un foro en línea llamado Zulip (****). Como primer paso, y para familiarizarse con las diversas herramientas y con formas de trabajo distintas de las habituales, su objetivo es digitalizar el programa del primer ciclo. Ya se ha realizado la mitad del trabajo. En este caso, «digitalizar» no significa «escanear documentos», sino introducirlos en Lean en un formato que este programa pueda entender. La ventaja es que Lean comprueba que la demostración propuesta es válida y coherente con las reglas de la lógica y los axiomas implementados.