Lean : un forum collaboratif
L’idée est simple : formaliser toutes les connaissances mathématiques dans un assistant de preuve libre et ouvert appelé Lean (https://leanprover.github.io).
Lean est ainsi un logiciel permettant la vérification de preuves mathématiques. Ce type de programmes a été utilisé pour la démonstration du théorème des quatre couleurs (voir les Graphes, Bibliothèque Tangente 54, 2015) ou encore la conjecture de Kepler sur l’empilement des sphères (voir Tangente 158, 2014). Un des assistants de preuve les plus utilisés est Coq, développé par l’Inria.
Lean est développé par Microsoft Research en C++ (Leonardo de Moura, 2013). Il est actuellement utilisé, entre autres personnalités, par Thomas Hales, le « tombeur » de la conjecture de Kepler.
Pour ce faire, les utilisateurs se réunissent sur un forum en ligne baptisé Zulip
(https://leanprover.zulipchat.com).
Pour commencer, prendre en main les divers outils et appréhender des modes de fonctionnement différents de leurs habitudes, leur premier objectif est de numériser le programme du premier cycle. La moitié du travail a déjà été accompli. Dans le cas présent, « numériser » ne signifie pas « scanner des documents », mais les introduire dans Lean sous un format compréhensible par ce logiciel. L’avantage est que Lean vérifie que ...
Lire la suite gratuitement