Comment abattre vos preuves

Quelles sont les directives générales pour vérifier vos preuves? Je crois que c'est important pour les étudiants diplômés comme moi. Je sais déjà ce que nous devons faire pour prouver quelque chose, mais vous devez toujours tout vérifier avant de l'envoyer. Même à votre propre conseiller.

J'ai élaboré moi-même des stratégies par essais et erreurs et j'ai reçu beaucoup de conseils de mon conseiller. Mais c'est toujours un travail très fastidieux. Normalement, quand vous avez fini avec quelque chose, vous voulez juste passer au problème suivant, mais vous devez toujours vous en tenir au problème actuel jusqu'à ce que tout soit parfait. Ici, je présente un exemple de ma propre liste d'astuces:

1. Remplissez les détails. Il y a beaucoup d'erreurs à certains endroits où vous écrivez "il est clair que ...", "sans perte de généralité ...", etc.
2. Essayez des chiffres. Essayez des cas extrêmes, comme "que se passe-t-il lorsque je mets ou n = 1000 ".$n=1$$n=1000$
3. Gardez un cahier propre. Ecrivez chaque jour dessus et comparez-le avec vos notes approximatives. J'essaie d'écrire aussi en latex, j'ai trouvé beaucoup d'erreurs de cette façon.

Quelles sont les stratégies générales que vous appliquez pour vérifier vos preuves?

L'objectif de cette question est d'en faire un wiki de communauté.

Les ingénieurs en logiciel ont une notion qu'ils appellent " odeurs de code ". Ce sont des symptômes dans le code qui peuvent indiquer un problème plus profond. Les ingénieurs en logiciel collectent des listes mentales d’odeurs à connaître (méthodes trop longues ou paramètres trop longs). Cela ne signifie pas nécessairement qu'il y a un problème, mais simplement que le rédacteur voudra peut-être vérifier.

Je propose que nous devrions également considérer "preuve odeurs" . Cela ne vous donnera pas un algorithme pour vérifier vos preuves, mais une langue et une métaphore pour reconnaître d'éventuels problèmes dans les preuves. Quelques exemples de preuves odeurs:

1. Les adverbes "clairement", "évidemment", etc.
2. Référence à la preuve d'un résultat précédent au lieu d'une référence au résultat lui-même.
3. Utilisation fluide d'un résultat avec de nombreuses conditions techniques préalables.

Il y a aussi des odeurs plus subtiles. Par exemple, si une preuve utilise le théorème binomial pour développer une expression, puis utilise ensuite le théorème binomial pour revenir à une forme fermée, il peut alors y avoir une manipulation directe sur la forme fermée qui donne le même résultat.

Ma suggestion est de rassembler une liste (mentale ou écrite) de telles odeurs et de les vérifier au fur et à mesure de la lecture de votre travail. Cette approche a pour effet de faire de vous un meilleur lecteur.

Note: Mon espoir dans cette réponse était de donner un côté intuitif à la réponse rigoureuse fournie par Comment écrire une preuve de Lamport, référencée dans la réponse de M. Alaggan.

Il y a un très bon article de Leslie Lamport ( Comment rédiger une preuve ). C'est en fait une proposition de sa part sur un style d'écriture d'épreuves détaillées de telle sorte que:

(1) Permet de détecter les erreurs de manière simple

(2) Indique clairement les hypothèses et les théorèmes utilisés dans quelles parties, ce qui permet de voir facilement ce qui se passe si vous souhaitez (par exemple) utiliser des hypothèses plus faibles

Il existe également une expérience communautaire et des commentaires inspirants sur cette technique sur MO, qui montrent une expérience positive en général (et quelques autres ressources également).

Mise à jour: il y a une nouvelle version Comment écrire une preuve du 21ème siècle .

Dick Lipton a un bel article intitulé " Comment prouver qu'une preuve est une preuve "

Il me semble me rappeler avoir lu il y a longtemps un compte rendu populaire sur la façon dont les physiciens traitent un problème analogue. Qui sait la précision de la version suivante? les corrections sont les bienvenues. Mais j'ai trouvé la stratégie sous-jacente assez remarquable.

Ils ont expliqué comment ils en étaient venus à croire aux trous noirs. Les trous noirs étaient à l’origine des constructions purement mathématiques, comme d’autres objets étranges de la physique comme des trous de ver. Leur stratégie était frappante: ils lanceraient mathématiquement d'autres objets sur l'objet à tester. Les trous de ver ont échoué à leurs tests car ils ont découvert que celui-ci s'effondrerait même en présence d'un objet physique normal, peut-être un astéroïde. Mais les trous noirs ont réussi ce test: le trou noir survivrait si un astéroïde lui était jeté. Alors ils ont essayé de jeter une étoile dessus. Même résultat. Finalement, ils ont jeté un autre trou noir au trou noir et celui-ci a survécu. En conséquence, ils sont devenus suffisamment confiants dans l’existence de trous noirs pour pouvoir commencer à les rechercher dans l’univers réel.

La pertinence et l’application de la stratégie ci-dessus consistent donc à commencer à jeter des éléments probants. Est-ce qu'il survit aux contrôles de bon sens ? Si vous supprimez une hypothèse nécessaire, est-ce qu'elle s'effondre comme il se doit? Est-ce qu'il s'effondre comme il se doit quand il est appliqué à des cas hors de sa portée? Résiste-t-il aux généralisations et aux spécialisations raisonnables? Consultez la liste des heuristiques de la section Comment résoudre ce problème de Polya . Essayez de transformer votre preuve avec ces heuristiques et voyez si elle est correcte et tombe comme il se doit.

Je pense que l’une des approches les plus sûres est de proposer de multiples preuves indépendantes. Ensuite, vous pouvez être sûr que votre résultat principal est correct, même si vous avez une erreur dans certains détails d'une preuve.

Une technique que j’ai trouvée utile consiste à réfléchir aux autres résultats que la stratégie de démonstration pourrait prouver. Si je suis facilement capable d'adapter la stratégie de preuve pour prouver un gros problème ouvert ou même un problème qui n'est pas ouvert, mais qui a une solution beaucoup trop compliquée comparée à la complexité de la stratégie de preuve, alors c'est une grande raison de douter la preuve.

Je revérifie toujours mes épreuves avec un correcteur d'épreuves tel que COQ ou ISABELLE . Si vous pouvez prouver votre preuve dans l’un de ces langages de programmation, vous pouvez être sûr que votre preuve est correcte. Aussi simple qu'un terme lambda;).