Technologie
Assistant de preuve
Lean est un logiciel qui vérifie des preuves écrites dans un langage formel, avec des règles précises. Il contrôle les étapes pour la question qui lui est fournie. Il faut aussi vérifier que cette question correspond au résultat annoncé.
Comprendre le mécanisme
Vérifier une preuve écrite dans des règles précises
Lean permet d’écrire une proposition et sa preuve dans un langage formel. Une proposition est l’affirmation à démontrer. Le logiciel vérifie que l’expression fournie constitue une preuve de cette proposition, dans le cadre des définitions et hypothèses utilisées.
Dans un exemple fictif, une équipe pourrait formaliser la règle disant qu’une commande payée et expédiée est payée. Elle vérifierait que la formulation écrite exprime bien cette règle. Une preuve acceptée ne dirait rien sur le paiement réel d’une commande particulière.
Preuve formelle et faits observés
Le contrôle porte sur la proposition formalisée. Il ne vérifie pas automatiquement que des hypothèses correspondent aux données du monde réel.
Dans un projet
Vérifier les étapes d’une preuve
Un chercheur peut écrire une preuve dans le langage de Lean pour que le logiciel vérifie ses étapes. Une proposition rédigée en langage courant doit d’abord être formalisée. Il faut contrôler que cette formalisation correspond bien à la question étudiée.
- Vous fournissez
- Règle fictive formalisée et preuve proposée pour cette règle.
- Vous contrôlez le résultat
- Preuve vérifiée ou erreur à résoudre dans la formalisation.
Exemple fictif. Il illustre un usage, sans résultat mesuré.
Les points à vérifier
Vérifiez la proposition formalisée et les hypothèses utilisées en plus du résultat du logiciel.
- Énoncé fidèleCompter les écarts entre la règle souhaitée et la proposition écrite.
- Hypothèses explicitesLister les affirmations admises et celles effectivement démontrées.
- Travail nécessaireMesurer le temps de formalisation et le nombre d’erreurs corrigées.
