Visites occasionnelles autour de preuves

Aujourd'hui, Ryan Williams a publié un article sur arXiv (précédemment publié dans SIGACT News) contenant une version moins technique de sa récente technique de limite inférieure ACC .

Ma question ne concerne pas la technique elle-même (bien sûr mérite des éloges), mais concerne le style du papier. Dans l'abstrait, il écrit:

La preuve sera décrite du point de vue de quelqu'un essayant de la découvrir.

Impressionnant! Dans la section Background, il ajoute:

Cet article est une discussion sur la façon de découvrir la preuve - une visite informelle autour de celle-ci. Tous les détails ne seront pas donnés, mais vous verrez d'où viennent toutes les pièces et comment elles s'emboîtent. Le chemin sera jonché de mes propres intuitions biaisées sur la théorie de la complexité - ce que je pense devrait ou ne devrait pas être vrai et pourquoi. Une grande partie de cette intuition pourrait bien être fausse; Cependant, je peux dire que cela m'a conduit dans une direction productive à au moins une occasion.

C'est incroyable et c'est la première fois que je le vois. Je me suis toujours demandé pourquoi les auteurs de papier n'écrivaient pas comment ils en étaient arrivés à la preuve, y compris les approches infructueuses qu'ils avaient essayées avant d'arriver à la piste qui avait conduit à la solution. Quand j'ai vu le papier de Ryan sur arXiv, je me suis senti très motivé pour le lire. Je le considère comme un papier révolutionnaire de ce point de vue. La plupart du temps, la seule chose que vous puissiez faire avec un papier est de vérifier son exactitude.

La question est la suivante:

• Êtes-vous au courant d'autres articles dans TCS où un résultat révolutionnaire est présenté sous la forme d'une "tournée informelle" plutôt que d'une série de lemmes techniques?

Je parle de publications dans des revues, pas de blogs ou de rapports techniques.

En outre, je l'ai étiquetée comme une grande liste , avec l'espoir qu'elle le sera réellement.

Il existe un article (2001) de style similaire rédigé par Lov Grover, qui décrit la voie à suivre pour son algorithme de recherche quantique révolutionnaire (1996).

Tim Gowers est un fan de ce genre de chose. Voir en particulier son exposé sur la méthode d'approximation de Razborov .

Dans son introduction, Gowers fait référence à mon article sur le forçage , qui est une tentative (pas tout à fait réussie) de faire la même chose pour le forçage. Le forçage est normalement considéré comme une technique de la logique et de la théorie des ensembles, mais il a parfois trouvé sa place dans le SDC. Il apparaît dans l’étude de la complexité arithmétique bornée et de la preuve propositionnelle (Krajíček et Takeuti sont deux chercheurs qui ont poursuivi ce lien), et le concept d’un oracle générique est lié au concept d’un filtre générique.

(Cela a commencé comme un commentaire et a pris beaucoup trop de temps).

Vous pouvez apprécier l'article de William Thurston sur la preuve et le progrès en mathématiques .

Les mathématiques ont en quelque sorte un langage commun: un langage de symboles, des définitions techniques, des calculs et une logique. Ce langage traduit efficacement certains modes de pensée mathématique, mais pas tous. Les mathématiciens apprennent à traduire certaines choses presque inconsciemment d'un mode mental à l'autre, de sorte que certaines déclarations deviennent rapidement claires. [...]

Les personnes familiarisées avec les manières de faire les choses dans un sous-champ reconnaissent divers modèles d’énoncés ou de formules comme idiomes ou circonlocutions pour certains concepts ou images mentales. Mais pour des personnes qui ne sont pas déjà au courant de ce qui se passe, les mêmes modèles ne sont pas très éclairants; ils sont souvent même trompeurs. La langue n'est vivante que pour ceux qui l'utilisent. [...]

Nous, mathématiciens, devons faire beaucoup plus d'efforts pour communiquer des idées mathématiques. Pour ce faire, nous devons accorder une plus grande attention à la communication, non seulement de nos définitions, de nos théorèmes et de nos preuves, mais également de nos façons de penser. Nous devons apprécier la valeur des différentes façons de penser à la même structure mathématique. Nous devons consacrer beaucoup plus d'énergie à la compréhension et à l'explication de l'infrastructure mentale de base des mathématiques - avec par conséquent moins d'énergie aux résultats les plus récents. Cela implique de développer un langage mathématique efficace dans le but radical de transmettre des idées à des personnes qui ne les connaissent pas déjà.

En ce qui concerne la question initiale, certains articles ne présentent pas d’idées dans le format Définition-Théorème Proof (DTP). Timothy Chow a quelques articles qui se concentrent sur la communication d’idées (bien qu’ils ne soient pas les premiers (ou les deuxièmes) articles sur le sujet / le résultat).

1. Vous auriez pu inventer des séquences spectrales , Timothy Chow, Notices of the AMS
2. Forcer pour les nuls , Timothy Chow

L'une des raisons possibles de la prévalence du format DTP est que nous en sommes tous habitués, à partir de livres et de journaux. Les réviseurs (et les lecteurs) trouvent parfois le style d’écriture non standard distrayant. Un moyen terme est constitué de papiers qui divisent doucement le lecteur en résultat. Il y a des papiers qui présentent un cas particulier ou un problème simple qui illustre l'idée générale.

1. La structure topologique de la calculabilité asynchrone , Maurice Herlihy et Nir Shavit. L'article présente de nombreuses illustrations et illustre l'idée générale d'un protocole simple avant d'appliquer le théorème principal à la résolution de problèmes non résolus.
2. $p$

Aucune discussion sur une présentation non standard d'idées remarquables ne serait complète sans mentionner le travail de Jean-Yves Girard . Unique est probablement le meilleur mot pour le décrire (sans être diplomatique ni sarcastique). De, la logique linéaire papier .

L'exégèse philosophique des règles de Heyting laisse en fait très peu de place à une discussion plus approfondie du calcul intuitionniste; mais est-ce que quelqu'un a déjà essayé sérieusement? En fait, la logique linéaire, qui est une extension claire et nette de la logique habituelle, peut être atteinte par une analyse plus claire de la sémantique des preuves (pas très loin de l'approche informatique et donc reléguée à la section suivante), ou par certaines considérations plus ou moins immédiates sur le calcul séquentiel. Ces considérations ont une signification géométrique immédiate, mais pour les comprendre, il faut oublier les intentions, en se souvenant, avec un dirigeant chinois, que ce n’est pas la couleur du chat qui compte, mais le fait qu’il attrape des souris.

Plus tard:

Il y a encore des gens qui disent que pour faire de l'informatique, il faut un fer à souder; cette opinion est partagée par les logiciens qui méprisent l'informatique et par les ingénieurs qui méprisent les théoriciens. Cependant, ces dernières années, la nécessité d'une étude logique de la programmation est devenue de plus en plus claire et le lien logique-informatique-science semble irréversible. [...]
D'une certaine manière, la logique joue le même rôle que celle de la géométrie vis-à-vis de la physique: le cadre géométrique impose certains résultats de conservation, par exemple la formule de Stokes. Les symétries de la logique expriment vraisemblablement une conservation profonde de l'information, sous une forme qui n'a pas encore été conceptualisée correctement.

Peut-être que les auteurs n'incluent pas ces tentatives infructueuses et l'histoire de la recherche dans leurs articles publiés en raison des contraintes imposées par les éditeurs et les membres du PC. Je suppose qu'il est très inhabituel pour un journal (et probablement encore plus pour une conférence) d'accepter un article dont l'essentiel est consacré à des tentatives infructueuses. Mais dans la plupart des cas, si vous parlez aux auteurs ou aux experts de la région, ils expliqueront l’histoire et les tentatives infructueuses (et beaucoup en parlent dans des ateliers).

J'ai vu plusieurs auteurs expliquer au moins d'où venaient les idées dans leurs papiers. Par exemple, Girard explique dans son article que l’idée de la logique linéaire est née de la recherche d’une sémantique dénotationnelle pour le OU intuitif. Vous pouvez trouver ce genre d’information également dans les monographies et biographies de chercheurs célèbres et dans des ouvrages qui leur sont consacrés ( l’autobiographie de Halmos et plus récemment «Kreiseliana: À propos et autour de Georg Kreisel », édité par Odifreddi, il existe également des volumes et des articles. dédié à certains théoriciens de la complexité). Espérons que davantage de personnes feront ce que Ryan a fait et expliqueront systématiquement le processus et raconteront l'histoire.

ps: vous pouvez les considérer comme une tradition de recherche orale :) (un peu similaire à la Torah orale qui n’a pas été autorisée à être écrite ).

Laszlo Babai (1990) a publié un article sous la forme d'une fable sur Arthur et Merlin décrivant la séquence dramatique qui a conduit la communauté au résultat IP = PSPACE de 1989, ce qui était bien incroyable un an auparavant.