Comment abattre vos preuves

59

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=1n=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é.

Marcos Villagra
la source
Si la question semble subjective, aidez-moi à l'améliorer.
Marcos Villagra
Comment puis-je créer ce wiki de communauté?
Marcos Villagra
1
Hé, cool! Je suis vraiment intéressé par les réponses à cette question. En outre, je peux apprécier votre # 3. (Quand j'y réfléchis, j'ai en fait des piles de papiers éparpillés partout quand je travaille intensément sur un problème, qui est ensuite déplacé au hasard. Beurk.) J'ai déjà rencontré une erreur de cette question et fini par gaspiller une bonne partie du temps.
Daniel Apon
@ Daniel: J'ai eu le même problème !! C'est pourquoi après avoir fini avec une épreuve, j'écris immédiatement la version en latex. Il est bon de savoir que je ne suis pas le seul gars en désordre qui garde tout partout :-)
Marcos Villagra
1
vous le signalez pour attirer l'attention du modérateur.
Suresh Venkat

Réponses:

39

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.

Don Sheehy
la source
4
Je le dis tout le temps à mes étudiants et ils pensent que je suis fou. Bien sûr, je prétends en fait pouvoir sentir un insecte, ce qui pourrait en partie faire partie du problème;)
Suresh Venkat
7
@Suresh: Cet étudiant pense que tu es fou pour différentes raisons. ;-)
John Moeller
4
Sur la note de code, les choses que j'essaie toujours de scruter dans les preuves des autres incluent les chaînes d'inégalité. Les erreurs les plus élémentaires ont souvent pour habitude de se glisser parmi les dérivations les plus difficiles.
John Moeller,
23

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 .

M. Alaggan
la source
5
Ces preuves sont très similaires à celles que l’on écrit dans un document de recherche PL. La chaîne de la logique est très explicite. Après avoir appris à lire et à apprécier les épreuves de style PL, j'ai eu du mal à comprendre les épreuves mathématiques "normales". De telles preuves exigent souvent que le lecteur pense de la même manière que l'auteur, et lorsque vous êtes habitué à un style de preuve différent, ce n'est tout simplement pas le cas (pour moi, du moins!)
Christopher Monsanto,
2
@Christopher Monsanto: PL signifie Langages de programmation? Je vous serais reconnaissant de bien vouloir citer un exemple (un de ces papiers) à vérifier :)
M. Alaggan,
5
J'ai toujours eu le sentiment que ce que Lamport suggère n'est pas compatible avec "Un lamentateur de mathématicien" de Paul Lockhart ( maa.org/devlin/LockhartsLament.pdf ).
Marcos Villagra
14

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.

Personne timide
la source
La plupart de votre réponse se concentre sur la vérification des preuves en vérifiant qu'elles deviennent fausses dans des situations où elles devraient l'être. Cela ne fonctionne pas car il ne vérifie pas que le théorème était vrai là où il était supposé être vrai! Par exemple, supposons que j'ai "prouvé" que chaque nombre impair est divisible par trois. Je vérifie que ma preuve échoue si j'étends aussi des nombres pairs: c'est le cas, car quatre n'est pas divisible par trois. Hourra, ma preuve doit être correcte!
David Richerby le
12

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.

Jukka Suomela
la source
9

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.

Opter
la source
5
PNP
6

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;).

Gopi
la source
Je n'ai jamais utilisé Coq, mais je devrais essayer. En fait, j'essaie de prouver certaines limites inférieures avec mathematica, mais je n'ai pas trouvé le bon moyen. J'ai peut-être besoin de forfaits spéciaux ou de quelque chose d'autre.
Marcos Villagra
1
Peut-être que c'est une longue attaque, mais si vous voulez prouver quelques limites inférieures avec des réels, vous pouvez vérifier ces bibliothèques: coqtail.sourceforge.net/?home/fr
Gopi,
D'accord, mais tout langage de programmation fonctionne. Le plus souvent, je fais cela à l'envers. Formulez le domaine problématique dans un langage de programmation (généralement Ruby), puis utilisez-le comme modèle pour ma preuve.
Chad Brewbaker