C'est l'idée de faire vérifier à un ordinateur qui est sale.
Et pourquoi donc ?
Je crois qu'il y a une confusion entre une preuve formelle en Coq, plus sûre qu'une preuve de maths à la main (et plus dure à produire, no free beer) et une « preuve » comme celle de 1976 pour le théorème des quatre couleurs où on a basiquement un gros programme Fortran qui calcule deux semaines et finit par répondre « OUI » ou « NON ».
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par auve . En réponse au journal Martin Gardner (1914-2010). Évalué à 3.
Et pourquoi donc ?
Je crois qu'il y a une confusion entre une preuve formelle en Coq, plus sûre qu'une preuve de maths à la main (et plus dure à produire, no free beer) et une « preuve » comme celle de 1976 pour le théorème des quatre couleurs où on a basiquement un gros programme Fortran qui calcule deux semaines et finit par répondre « OUI » ou « NON ».