Ceci est ma première question sur la pile cstheory, alors ne soyez pas trop impoli si je viole l'étiquette d'une manière ou d'une autre)
Comme nous le savons, en mathématiques, même des mathématiciens, des superstars et des génies célèbres font de temps en temps de graves erreurs. Par exemple, le théorème à 4 couleurs et le théorème de Fermat nous fournissent des cas dramatiques de la façon dont même les esprits les plus brillants peuvent être trompés. Cela peut même prendre des années pour prouver l'inexactitude de certaines preuves de falsification.
Ma question est - pouvez-vous fournir des exemples remarquables de telles erreurs en informatique? Je ne sais pas, quelque chose comme "Le Dr X a prouvé en 1972 qu'il était impossible de faire Y en moins de O (log n), mais en 1995, il s'est avéré qu'il avait en fait tort".
la source
Réponses:
Un exemple tristement célèbre en géométrie informatique est la preuve incorrecte du théorème de zone pour les arrangements d'hyperplan publié par Edelsbrunner, O'Rourke et Seidel [FOCS 1983, SICOMP 1986]. La preuve apparaît également dans le manuel de géométrie computationnelle de 1987 d'Edelsbrunner.
Le théorème de zone est une étape clé dans la preuve que l'algorithme incrémentiel récursif standard pour construire un arrangement de hyperplans dans R d s'exécute en temps O ( n d ) .n Rré O ( nré)
En 1990, Raimund Seidel a découvert que la preuve publiée était incorrecte, après avoir été contestée sur un point technique subtil par un étudiant de sa classe de géométrie computationnelle. Pendant ce temps, une énorme littérature sur la recherche d'hyperplans / demi-espace / simplex / semi-algébrique avait été développée, qui s'appuyait toutes sur le temps de construction pour les arrangements, qui à leur tour s'appuyaient sur le théorème de zone. (Aucun de ces auteurs n'a remarqué le bogue. Raimund avait enseigné la "preuve" publiée en détail pendant plusieurs années avant qu'il ne soit mis au défi.)O ( nré)
Heureusement, Edelsbrunner, Seidel et Sharir ont presque immédiatement trouvé une preuve correcte (et beaucoup plus simple!) Du théorème de zone [Nouveaux résultats et nouvelles tendances dans CS 1991, SICOMP 1993].
la source
Le protocole de cryptographie à clé publique Needham-Shroeder, un protocole à 5 lignes, s'est révélé non sécurisé 17 ans après sa publication. C'est l'exemple préféré des personnes chargées de la vérification pour effectuer une analyse formelle des protocoles de cryptographie.
la source
Dick Lipton a publié un nouveau billet sur la non-monotonie des connaissances mathématiques, et il y documente des exemples de revendications qui se sont révélées fausses, ou du moins nécessitaient une correction.
la source
Il y a eu des conjectures qui se sont révélées fausses (par exemple, une distorsion constante incorporant des métriques de type négatif réfutées par Khot et Vishnoi), mais il n'y a rien de mal à poser une fausse conjecture car après tout, c'est une conjecture.
la source
"J'ai été choqué d'apprendre que le programme de recherche binaire que Bentley a prouvé correct et testé par la suite dans le chapitre 5 de Programming Pearls contient un bogue. Une fois que je vous dirai ce que c'est, vous comprendrez pourquoi il a échappé à la détection pendant deux décennies. De peur que vous ne pensiez Je choisis Bentley, laissez-moi vous dire comment j'ai découvert le bogue: la version de la recherche binaire que j'ai écrite pour le JDK contenait le même bogue. Il a été signalé à Sun récemment lorsqu'il a interrompu le programme de quelqu'un, après avoir attendu neuf ans ou plus. "
-
Joshua Bloch "Extra, Extra - Lisez tout à ce sujet: presque toutes les recherches binaires et fusions sont brisées" 2006
la source