
Traduire les mathématiques en preuves formelles vérifiables grâce à l'apprentissage automatique
Ce que la machine traduit, et ce qu’elle tait Dans le langage informatique Lean4, il existe un mot qui devrait, en bonne logique, n’avoir aucune place : sorry. Emprunté …


