isabelle

Le débat sur l'avenir du langage Lean dans la recherche mathématique

• Une discussion sur MathOverflow interroge la pérennité du langage Lean pour les preuves mathématiques.
• Les chercheurs débattent de ses limites et alternatives face à des outils comme Coq ou Isabelle.
• Ce débat reflète les enjeux de standardisation dans la formalisation des mathématiques.