Une preuve finie

Je tiens à préciser que ce billet sera surement incompréhensible, même pour les matheux/informaticiens, même pour les scientifique. J'espère, à minima, qu'il sera encore compréhensible pour moi dans quelques années, pour que je puisse revivre l'extase que j'ai au moment de l'écriture - je n'en suis malheureusement pas sûr. Je ne force jamais qui que ce soit à me lire, cette fois-ci, je vous en décourage même vivement. Où alors, dites vous que c'est à la manière du «Théorème Vivant», de Villani, le but est plus de voir ce qui se passe dans la tête du matheux que de comprendre les maths. Je sais pas. Bon, rentrons dans le billet.

En aout 2013 j'avais fini une preuve de 30 pages, avec des «il est clair que», et quelques fois c'était faux. Déjà, car ce n'était jamais clair, à part pour moi. Mais surtout car il arrivait que le résultat «clair» soit faux. Encore qu'il n'ait jamais été que faux de peu, il était toujours presque vrai. Il suffisait de quelques petites modifications pour que ça soit vrai. Mais les mathématiques n'admettent pas ces petites approximations.

Ce soir j'ai enfin fini sans aucun «clair que», en étant totalement sûr de chaque partie de chaque lemme. 130 pages. Bon, il y a aussi des rajouts d'intuitions, d'explications, d'exemples, quelques (19) figures, 2 pages et demi d'index... Mais une bonne grosse partie de cette nouvelle centaine de page vient des preuves. Pour donner une idée, il y a 35 exemples, 61 définitions, 15 notations, 115 lemmes, 7 propositions, 3 théorèmes et 3 algorithmes.


En mai 2013, j'avais implémenté et testé les algorithmes. C'est 5000 lignes en oCaml, plus 1000 de commentaires.

Je crois que ce qui m'impressionne le plus, c'est que malgré ces 2 ans de fautes et d'erreurs corrigés dans la démonstration, l'algorithme fonctionnait, et n'a pas besoin d'être modifié. Autrement dit, il s'agit de deux ans à régler des détails, mais où le gros du travail était déjà fini. Bon, c'est aussi deux ans à apprendre à améliorer ma rédaction.

Déjà, c'est une chance énorme, parce que, des grosses preuves, qui doivent être jeté à la poubelle à cause d'un lemme improuvable, l'histoire en regorge, les doctorants en ont plein. Je dois même dire que, pendant plus de deux mois, j'ai eu peur d'être dans cette situation. Il y avait un lemme, une partie vraiment technique, une égalité que je n'arrivai pas à prouver. Je me suis mis à peaufiner tout les résultats autours, tout le reste du papier, revenant plusieurs fois dessus, et toujours bloqués. Avant d'abandonner la belle technique que j'avais développé, et qui marchait partout SAUF pour cette égalité, et de faire ce qui m'effrayait et me semblait vouer à l'écher, prouver cette égalité «à la main».


C'est une expression que je trouve marrant «à la main», je ne sais pas si elle est courante chez les mathématiciens, où si c'est une spécificité de mon entourage. Parce que, d'abord, je n'écris jamais à la main, je fais toujours tout directement en LaTeX (sauf les dessins). Prouver une égalité «à la main», par exemple, ça veut dire que je ne vais pas utiliser de lemme, encore moins de théorème, qui permet de déduire l'égalité. Mais qu'à la place, je fais faire tout le calcul, en détaillant explicitement la totalité des cas envisageable, en remontant à la définition, et en s'arrêtant quand on utilise les axiomes ou les hypothèses.


Prouver ce lemme, cette égalité, «à la main» était une expérience assez bizarre. D'abord car la preuve prend 8 pages, et que je n'ai jamais utilisé de preuve de 8 pages pour un lemme[1]. Mais surtout, parce que, au moment où j'étais bloqué, j'avais quand même la certitude que ce lemme était vrai. Déjà, j'ai passé des heures à chercher un contre-exemple, sans trouver la moindre piste de début d'idée de comment rendre le lemme faux.

Les contre-exemple ont détruit une dizaine de mes lemmes, au moins, me forçant à les modifier, pour tenir compte des cas que j'avais oubliés. Mais souvent, ces contres exemples étaient assez naturels, je ne crois jamais avoir eu besoin de recourir à des cas tarabiscotés. Mes contre exemples sont des formules logiques, et en général, c'était carrément des prédicats atomiques, ou alors la conjonction de deux prédicats atomique dans le pire des cas. Ou alors, mes contre exemple ont été trouvé quand je codai, et que oCaml me levait une exception, montrant que j'avais oublié de vérifier qu'un élément existe avant de l'utiliser. Mais là, j'avais fait le tour des formules vraiment simple, mon programme fonctionnait aussi bien sur les exemples simples que sur des exemples aléatoires, et RIEN.

Pire, chaque exemple me montrait encore plus que l'égalité était «naturelle». Et d'ailleurs, sémantiquement, il y avait une raison d'être à cette égalité. L'égalité était certes très complexe à exprimer, une expression composés de diverses sous expression, elle même composées de sous expression[2], mais elle ne sortait pas du chapeau. Je ne m'amusais pas à supposer que cette égalité était juste car «c'est ce qui fait que ça fonctionne», mais j'étais à peu près capable d(e m)'expliquer l'intuition derrière cette égalité, de ce qu'elle signifiait en vrai(d'ailleurs, cette explication est donné à côté de l'égalité.)

Malheureusement, ça m'arrive, dans ce papier, de donner des égalités «juste parce que c'est vrai, et que j'en ai besoin», sans vrai raison derrière. Ça m'arrive une seule fois, mais pour une liste de 17 égalités. Qui sont toutes relativement simple d'ailleurs. Mais là, c'était une égalité compliquée, mais, à la limite, je pourrai presque dire qu'elle était si naturelle que, même si elle ne servait à rien, j'aurai trouvé justifié de la prouver car elle était jolie. Ce qui rendait d'autant plus frustrant d'être bloqué.

Quelque part, je dirai que je devais avoir «foi» en cette égalité, parce que je continuais de baser une bonne partie de mon travail sur elle, alors qu'elle n'était pas prouvé. J'ai pendant ce temps chercher à trouver une autre voix pour pouvoir poursuivre sans cette égalité, mais toutes les autres voix auxquels je pensais était, fondamentalement, la même que cette égalité, et j'étais bloqué pour des raisons à peu près similaire. Pour prendre l'exemple classique de la montagne, j'étais à la base, je voulais atteindre un sommet. Certes, j'ai finalement abandonné l'idée de grimper directement en ligne droite. Mais d'une façon où d'une autre, il y a bien un moment où il a fallu que je monte, même si utiliser des routes de faible pente (preuve à la main), fait que c'était CONSIDÉRABLEMENT plus long que si j'avais pu utiliser un mécanisme automatique (télésiège/lemme).

C'est aussi un sentiment horrible, de savoir que tant tiens sur de la foi, alors que je suis matheux. D'un côté, je n'osais pas trop y penser, je ne savais pas si le plus horrible était de me dire qu'il est possible que cette centaine de page finisse à la poubelle. Me dire qu'on a passé un an pour rien avec mon directeur de thèse, à relire la première cinquantaine de pages [3]. Ma thèse serait pas totalement gâché, j'ai déjà un papier d'accepté dans un journal, un autre présenté en conférence, et quelques autres résultats. Mais ça aurait supprimé la moitié du travail de ces 3 ans et demi. Et même si, scientifiquement, c'est acceptable de se tromper, pour la soutenance de thèse, pour le manuscrit, ça ne le fait pas trop. Il me semble que, théoriquement, un scientifique expérimental peut dire «on a émis tel hypothèse, on a testé, et en fait non», ça rajoute de l'information pertinente, pour dire que quelque chose est faux. Mais une fausse preuve de A n'est en aucun cas une preuve de non A.

Je n'en suis pas fier, mais dans des moments comme ça, j'hésitais à juste donner l'intuition de pourquoi ça doit marcher, rajouter un «il est clair que», et puis tenter le diable, attendre de voir si quelqu'un tique. C'est aussi à ce moment là que je me demande «alors, pourquoi tu fais des maths», parce que c'est vraiment triste si le fait de devoir publier le théorème et soutenir la thèse prend le pas sur le fait d'avoir une vérité mathématique correctement établie.


Le plus incroyable pour moi, et je ne pense pas être capable de partager cet admiration, c'est que tout tient. Le fait que j'ai, en 2013, pu implémenter un algorithme correcte dont la preuve était fausse, montre que l'idée générale, je la maîtrise depuis un moment.

L'idée générale, c'est que j'étudie des ensembles de vecteurs(tuple), de nombre entiers. À la base, ils sont représenté par une méthode abstraite, un «automate fini». Et je veux voir si je peux les transformer en un autre formalisme abstrait: des formules de logiques, avec des prédicats arithmétiques faibles(modulo et relation d'ordre). Donc mon but est de passer d'une abstraction à une autre. Et pour cela, j'étudie les automates, j’abstraie des propriétés, pour pouvoir regarder juste certains automates qui, moralement, représentent tous les automates qui m'intéressent. Puis j’abstraie encore pour transformer les «mots» en des «partition totalement ordonnées». Puis j’abstraie encore pour remplacer «totalement» par «partiellement ordonnées».

À la fin, je fais des calculs sur les partitions partiellement ordonnées(on va dire POP pour faire court), et je ne considère plus que ça. Et j'obtiens ma preuve, oubliant totalement les ensembles de vecteurs de nombres, qui sont pourtant les objets qui m'intéressent au départ. J'ai beau être matheux, je trouve incroyable de pouvoir travailler sur une abstraction d'abstraction d'abstraction d'abstraction. Le problème, étant, je le constate quand on relit avec mon directeur, qu'il peut arriver que le lecteur ne voit plus le rapport entre l'objet théorique utilisé et ce qui voulait être fait à la base, et que, par conséquent, au lieu de sembler aller vers le résultat que je veux prouver, les lemmes techniques semblent être des pures exercices formels sans signification.

Exercice formel, car j'ai beaucoup de formalisme. Une POP, c'est un quadruplet, contenant un nombre, un vecteur de nombre, un vecteur de symboles et une matrice d'autres symboles. Et ce quadruplet satisfait 16 axiomes. En vrai, dire 16 axiomes, c'est arbitraire, je pourrai prendre un seul axiome qui est la conjonction de mes 16 axiomes actuels. Je pourrai aussi découper un axiome en morceau. Ce qui est important, c'est que c'est une grosse structure. Ce n'est pas une structure complexe, il y a un nombre fini de POPs qui existent[4], les algébristes, les combinatoriciens, manipulent régulièrement des structures beaucoup plus fines, beaucoup plus compliquées. C'est juste que décrire explicitement une POP prend de la place, et prouver que le quadruplet est un pop nécessite, pour être formel, de montrer que les 16 axiomes sont respectés. Et je ne compte pas le nombre de fois où j'ai écrit «il est clair que P est un POP», et où en fait, un axiome n'était pas respecté. 15 axiomes étaient respectés, mais pas le 16 ème. Ce n'était d'ailleurs pas tout le temps le même, même si en général, c'est le côté «ordonné» qui buggait. Quoi que pour être honnête, je n'écrivai jamais «il est clair que P est un pop», je disais juste «Soit P le pop suivant:»... et ce qui suivait n'était pas une POP, mais juste un truc qui ressemblait à une POP à un axiome près.

L'ensemble des POP forme un semi-groupe, autrement dit, on peut prendre deux POP, les additionner, et obtenir un troisième POP. Et c'est là que, pour moi, le sentiment de fantastique apparaît. Parce qu'à partir du moment où on peut les additionner, on peut écrire des égalités, des équations. D'ailleurs, l'égalité qui me posait problème, dont je parlais plus haut, c'est une égalité entre POP. Et quand certaines égalités sont prouvés, ça montre que l'abstraction est correcte, ça donne l'impression que c'était LE bon choix. Ce n'est pas tout à fait un «raisonnement divin»/une preuve du LIVRE, parce que le sujet n'est pas assez fondamental pour mériter d'y avoir sa place, mais tout de même pas loin. Ça tombe juste, pile poil. La preuve, je me sers de chacun des 16 axiomes, et je peux montrer que, pour tout POP, pour tout quadruplet respectant ces 16 axiomes, il y a un cas utilisant ce POP, donc je ne peux PAS rajouter quoi que ce soit aux 16 axiomes, et je ne peux rien retirer.

Et non seulement ça me fait ça pour les 16 axiomes, mais j'ai une deuxième liste, qui contient 8 propriétés que doivent vérifier un automate (une des deux abstractions qui m'intéressent), pour représenter un ensemble qui est aussi descriptible par une formule logique. Et encore une fois, le côté, «si et seulement si» me semble merveilleux. Arriver à dire que, dès qu'on satisfait ces propriétés, il y a une formule, ça implique qu'on ne peut pas rajouter un peu plus de limite. Et dire que dès qu'il y a une formule, ces propriétés sont satisfaites, ça veut dire qu'on ne peut rien retirer. Je ne suis presque plus capable de dire comment j'ai réalisé ce miracle, comment j'ai pu lister ces propriétés si exacte.

C'est un regret que j'ai, après 3 ans à travailler sur ce résultat, je connais la preuve sur le bout des doigts, je suis capable de redonner le schéma globale des 130 pages de tête, ou de reparler de chaque partie assez facilement. Par contre, j'ai totalement oublié le chemin pris pour arriver à cette preuve. Je sais que je suis passé par des notions que j'ai introduites[5], qui ont disparu, et dont je ne me souviens que du nom. Je sais que j'avais utilisé des ensembles d'axiomes légèrement différents, que j'ai souvent changer le plan globale du papier. Mais je ne me souviens plus de tout, et malgré l'historique que j'ai gardé (vive GIT), je pense que je ne relirai jamais les versions d'avant.

Le point qui n'a jamais changé, en tout cas, c'est le temps de calcul. Depuis le début, j'avais un truc rapide. Et je trouve ça assez fantastique. Chacune des 8 propriété susmentionnées peut se tester en temps O(n log(n)). I.e. rapidement. Donc en plus d'être mathématiquement joli, c'est efficace (je sais, je l'ai implémenté, et testé !) Et je ne vois pas de raison pour que ça doive être efficace, après tout, avec une preuve si longue, compliquée et tarabiscotée, je pourrai m'attendre à ce que ce soit lourd. Mais en fait non. En fait, c'est la première fois que je vois si intimement la notion «une preuve, c'est un algorithme», parce que ma preuve est un énorme algorithme, un algorithme en temps double exponentielle. Mais une fois retiré tous les calculs qui ne servent qu'aux mathématique, une fois que seul les calculs utiles sont gardé, c'est rapide.


Plus haut, je disais que j'avais fini la preuve. Il me reste encore pas mal d'effort de rédaction à faire. Je vais avoir besoin de plein de relecture de ces 130 pages, sans compter celle que me fait mon directeur de thèse. Bref, je suis loin d'avoir fini. Mais, là. Je suis content.

Notes

[1] Malheureusement, j'ai déjà lu un papier avec ce genre de preuve. C'est horrible, et je suis encore à la recherche de moyen de découper en plus petit morceau, mais ça semble impossible.

[2] et que j'ai du simplifier par la suite, suite à la haine de mon directeur de thèse - et de thoute personne sensée, pour les formules qui contiennent des indices d'indices d'exposants d'indices d'exposants...

[3] j'écris vraiment très mal, et j'ai du repasser au moins 3 fois par pages sur les 30 premières.

[4] enfin, quand certains paramètres sont fixés.

[5] la réécriture de partition partiellement ordonnée

Commentaires

1. Le mardi 23 février 2016, 15:25 par Athreeren

Je n'ai jamais lu une thèse de mathématiques ; je ne pensais pas que l'intégralité de la thèse pouvait être seulement la démonstration d'un seul théorème. Parce que si tu es déjà à 130 pages, il ne doit plus rester grand chose à ajouter, si ?

"suite à la haine de mon directeur de thèse - et de thoute personne sensée, pour les formules qui contiennent des indices d'indices d'exposants d'indices d'exposants"
Il y a des formules qui sont plus lisibles depuis la source de LaTeX que du document final...

"Je n'en suis pas fier, mais dans des moments comme ça, j'hésitais à juste donner l'intuition de pourquoi ça doit marcher, rajouter un «il est clair que», et puis tenter le diable, attendre de voir si quelqu'un tique. C'est aussi à ce moment là que je me demande «alors, pourquoi tu fais des maths», parce que c'est vraiment triste si le fait de devoir publier le théorème et soutenir la thèse prend le pas sur le fait d'avoir une vérité mathématique correctement établie."
Rien que pour ce paragraphe, ça vaut le coup de lire cet article. C'est intéressant de voir que ce genre de choses arrive aussi à des gens biens.

2. Le lundi 7 mars 2016, 13:53 par LCF, philosophia naturalis

Hygiène scientifique: toujours tenter de démonter à la barre à mine ce que l'on avance, pour éviter de raconter des conneries. Si ça tient le coup, ce n'est pas quelque chose qui s'écroulera à la première brise venue.

On apprend beaucoup en désossant ce qui fonctionne et en se demandant pourquoi.

3. Le samedi 26 mars 2016, 15:32 par N

Jeanne Siauf-Facchin dans son bouquin «trop intelligent pour être heureux ?» explique qu'elle a rencontré pas mal de «zèbres» (des gens qui ont des soucis avec leur cerveau qui turbine tout le temps), et que ces zèbres ont en commun quelque chose de saisissant : ils ont acquis une conviction profonde, et sont mal à l'aise quand on leur demande d'expliquer cette conviction.

Elle sous-entend dans un paragraphe que dans le cerveau, ça se passerait comme ça : une info est «calculée» à partir d'éléments, grâce à de la «matière blanche» (tout ça semble scientifique sur le papier mais je n'ai pas les mots précis), et qu'en gros, ensuite, le cerveau oublie les connexions ultra-rapides qui ont abouti à la conclusion. Bref, elle décrit l'intuition comme le résultat de deux processus concurrentiels dans le cerveau : les processus qui vont de A à B ne sont pas les mêmes que les processus «intuitifs». Elle ajoute que les processus intuitifs ont tendance à ne pas laisser de traces de leur naissance.

Je te conseille par ailleurs la lecture de ce livre qui m'a pas mal aidé à comprendre ce que je fais et ce que j'ai fait dans ma vie.

Ajouter un commentaire

Le code HTML est affiché comme du texte et les adresses web sont automatiquement transformées.

Fil des commentaires de ce billet