Lean

Lean est un assistant de preuve. Vous y écrivez un raisonnement mathématique, puis le logiciel en vérifie chaque étape selon les règles de la logique. S’il compile, la démonstration est correcte, sans qu’un relecteur ait à accepter quoi que ce soit sur parole. Les mathématiciens l’utilisent depuis des années pour formaliser de grands théorèmes.

Lean est devenu important pour l’IA pour une raison précise. Lorsqu’un modèle affirme avoir démontré un résultat, un certificat Lean transforme cette affirmation en fait vérifiable plutôt qu’en question d’interprétation. C’est pourquoi les laboratoires publient désormais leurs preuves en Lean en plus de leur version rédigée.