Qu’est-ce qu’une erreur mineure ?

Qu’est-ce qu’une erreur mineure ?

Points clés

1. Si une erreur dans une définition ou une démonstration est difficile à repérer, même si elle est facile à corriger, alors cette erreur n’est pas mineure.
2. Certaines erreurs ne peuvent être détectées qu’avec l’aide d’un assistant de preuve.

Résumé

• De décembre dernier jusqu’au 16 avril de cette année, j’ai consacré environ 170 heures à démontrer le théorème sur les chaînes String.splitOn_of_valid dans la bibliothèque standard de l’assistant de preuve Lean.
• Au cours de cette démonstration, j’ai découvert un bug dans la définition de la fonction String.splitOn.
• Corriger ce bug n’a pas été très difficile. Il suffisait de remplacer i par i - j dans cette définition.
• Mais cela ne veut pas dire que cette erreur était une simple bévue mineure. Selon cette définition, la fonction splitOn fonctionne généralement correctement, mais produit des résultats erronés dans certains cas particuliers.
• Sans un assistant de preuve comme Lean, je n’aurais jamais pu trouver une erreur aussi subtile.