- Die Übertragung des FLT-Beweises nach Lean läuft seit zwei Monaten. Die Definitionen von R und T, die für Wiles’ „R=T“-Theorem nötig sind, sind noch nicht fertig, aber ein Ergebnis aus der abstrakten kommutativen Algebra wurde bereits bewiesen
- Ziel ist nicht, den ursprünglichen Beweis aus den 1990er-Jahren exakt zu replizieren, sondern auf Lean und mathlib einen durch spätere Arbeiten von Diamond/Fujiwara, Kisin, Taylor, Scholze u. a. verallgemeinerten und vereinfachten Beweis aufzubauen
- Bei der Formalisierung der für den modernen Beweis nötigen crystalline cohomology zeigte sich ein Problem: In Robys Aufsatz von 1965, der Standardliteratur zu divided-power-Strukturen, scheint ein zentrales Lemma falsch zu sein
- Brian Conrad fand im Anhang des Buchs von Berthelot-Ogus einen alternativen Beweis; auch Arthur Ogus antwortete, er wisse, wie man die Fehler in diesem Anhang beheben könne, sodass das Projekt wieder vorankommen kann
- Der Fall zeigt, wie riskant es ist, dass Detailbeweise in der modernen Mathematik auf Expertenwissen und implizitem Wissen beruhen, und stärkt den praktischen Grund, Beweise in formalen Systemen festzuhalten
Aktueller Stand der Übertragung des FLT-Beweises nach Lean
- Die Arbeit, einem Computer den Beweis von Fermats letztem Satz (FLT) beizubringen, läuft seit zwei Monaten
- Für das „R=T“-Theorem, den Kern von Wiles’ Beweis, ist viel Arbeit nötig, um in Lean zu definieren, was R und T sind; beide Definitionen sind noch nicht abgeschlossen
- Der PhD-Student Andrew Yang hat bereits das nötige Ergebnis aus der abstrakten kommutativen Algebra bewiesen
- Es hat die Form: „Wenn abstrakte Ringe R und T mehrere technische Bedingungen erfüllen, dann sind sie gleich“
- Der aktuelle Entwurf ist als blueprint öffentlich verfügbar
- Verwendet werden Lean und die Mathematikbibliothek mathlib
- Wer etwas Lean und Zahlentheorie kennt, kann sich über die contribution guidelines, das project dashboard und die Issues beteiligen
Warum der Beweis aus den 1990er-Jahren nicht einfach übertragen wird
- Das Projekt formalisiert Wiles’ Beweis aus den 1990er-Jahren nicht unverändert
- Durch spätere Arbeiten von Diamond/Fujiwara, Kisin, Taylor, Scholze und anderen wurde der Beweis stärker verallgemeinert und vereinfacht
- Ziel ist nicht nur, FLT zu beweisen, sondern auch allgemeinere und stärkere Resultate in Lean aufzubauen
- Falls eine KI-Revolution in der Mathematik tatsächlich stattfindet und Lean ein wichtiger Baustein davon wird, kann es hilfreich sein, wenn Computer die zentralen Definitionen der modernen Zahlentheorie in einer verständlichen Form vorliegen haben
Divided powers, die für crystalline cohomology nötig sind
- Der zu formalisierende Beweis verwendet crystalline cohomology, die in Wiles’ ursprünglichem Beweis nicht vorkam
- Diese Theorie wurde in den 1960er- und 1970er-Jahren in Paris entwickelt; auf Grundlage von Grothendiecks Ideen legte Berthelot ihre Fundamente
- Klassische Exponential- und Logarithmusfunktionen sind wichtig für das Verständnis der Differentialgeometrie und der de Rham cohomology, funktionieren in arithmetischen Situationen wie characteristic p aber nicht unverändert
- Divided power structures, die in Robys Arbeiten aus den 1960er-Jahren entwickelt wurden, spielen eine Schlüsselrolle beim Aufbau ähnlicher Funktionen, die in arithmetischen Situationen nutzbar sind
- Um Lean crystalline cohomology beizubringen, müssen zuerst divided powers formalisiert werden
Das bei der Lean-Arbeit sichtbar gewordene Problem in Robys Literatur
- Antoine Chambert-Loir und Maria Ines de Frutos Fernandez arbeiteten daran, die Theorie der divided powers in Lean zu formalisieren
- Im Sommer deckte Lean ein Problem in der menschlichen Argumentation der Standardliteratur auf; nach Prüfung schien ein zentrales Lemma in Robys Arbeit falsch zu sein
- Technisch entwickelt Berthelots Aufsatz die Theorie der divided powers nicht von Grund auf, sondern verwendet Robys „Les algebres a puissances divisees“
- Der Aufsatz erschien in Bull Sci Math, 2ième série, 89, 1965, S. 75–91
- Lemme 8 auf S. 86 scheint falsch zu sein, und es war nicht klar, wie der Beweis zu reparieren wäre
- Dieser Beweis zitiert ein anderes Lemma aus Robys Ann-Sci-ENS-Aufsatz von 1963 falsch
- Die korrekte Aussage lautet
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R), aber bei der Anwendung fehlte ein Tensorprodukt
- Dieses Problem zerstörte Robys Beweis, dass die divided power algebra eines module über divided powers verfügt, und blockierte damit die Definition des Rings
A_cris
Eher „der Beweis hat eine Lücke“ als „die Theorie ist falsch“
- Das bedeutet nicht, dass crystalline cohomology selbst im Wesentlichen falsch wäre
- Die Hauptsätze scheinen weiterhin richtig zu sein, aber der Beweis, dem Antoine und Maria Ines folgten, war unvollständig
- Roby, Grothendieck und Berthelot sind alle verstorben, daher konnte man die ursprünglichen Experten nicht direkt fragen
- Mehrere Fachleute gehen davon aus, dass sich der Beweis der Hauptergebnisse reparieren lässt, auch wenn ein Zwischenlemma falsch ist
- Für eine Formalisierung reicht die Einschätzung „das lässt sich wohl reparieren“ nicht aus; gebraucht wird ein tatsächlich reparierter Beweis
Der Umweg, den der Anhang von Berthelot-Ogus eröffnete
- Tadashi Tokieda erzählte Brian Conrad in Stanford von dieser Geschichte, woraufhin Conrad fragte, was es mit der Behauptung auf sich habe, crystalline cohomology sei falsch
- Nachdem er die technischen Details gehört hatte, stimmte Conrad zu, dass es nach einem Problem aussehe, und begann mit der Prüfung
- Einige Stunden später teilte Conrad mit, dass es im Anhang des Buchs von Berthelot-Ogus über crystalline cohomology einen anderen Beweis dafür gebe, dass die universal divided power algebra of a module divided powers besitzt
- Aus Conrads Sicht sah dieser Ansatz in Ordnung aus, und dadurch konnte der Beweis wieder vorankommen
- Als später bei einem Mittagessen mit Arthur Ogus in Berkeley erzählt wurde, dass dieser Anhang das Problem gelöst habe, antwortete Ogus, dass auch dieser Anhang mehrere Fehler enthalte, er aber wisse, wie man sie beheben könne
Warum die moderne Mathematikliteratur Formalisierung braucht
- Dieser Prozess zeigt, dass die Art, wie Menschen moderne Mathematik dokumentieren, möglicherweise nicht robust genug ist
- Viele Fakten bleiben als „Dinge, die Experten wissen“ bestehen und sind in der Literatur möglicherweise nicht exakt ausgearbeitet
- Wichtige Ideen mögen robust genug sein, solche Erschütterungen zu überstehen, doch die tatsächlichen Detailbeweise befinden sich nicht immer dort, wo man sie erwartet
- Wenn Mathematik korrekt in formalen Systemen festgehalten wird, lässt sich die Fehlerwahrscheinlichkeit stark verringern
- Auch für Mathematiker, die keine Formalisten sind, gilt: Wenn Maschinen menschliche Argumentationen lernen und selbst Mathematik betreiben sollen, muss man ihnen diese Argumentationen zuerst beibringen
- Maria Ines hielt im Cambridge Formalization of Mathematics seminar einen Vortrag über die Formalisierung von divided powers; die genannten Probleme gelten als geklärt
- Das Projekt ist wieder auf Kurs, doch es bleibt möglich, dass die Literatur erneut zum Hindernis wird
1 Kommentare
Hacker-News-Kommentare
Ich erinnere mich daran, wie ich in der Graduiertenzeit schnellen Code schrieb, um den rechnerischen Ansatz meines Betreuers zur Birch–Swinnerton-Dyer-Vermutung zu unterstützen.
Bei einem Zahlentheorie-Seminar in einer nahegelegenen Stadt wurde ich gefragt, ob es darum gehe, die Belege für die Vermutung zu stärken. Ich antwortete lachend: „Nein, ich würde lieber ein Gegenbeispiel finden“, worauf die Experten ziemlich wütend wurden.
Die Zahlentheorie ist so alt und tief, dass eine Dissertation in diesem Gebiet fast erst der erste Schritt dazu ist, Anfänger zu werden; auch wenn ich Notation und Definitionen kannte, reichte das nicht bis zur darunterliegenden Intuition.
Deshalb hinterließ die Wut der Experten über meine Aussage, ich hoffe auf ein Gegenbeispiel, eher Neugier als Angst, und ich fragte mich, was sie sahen, das sie noch nicht in Worte fassen konnten.
Solche Fortschritte bei der Formalisierung machen Mathematik für Menschen, denen Programmieren vertrauter ist, deutlich zugänglicher.
Die Sorge über mangelnde Formalität ist berechtigt, aber die richtige Reaktion auf Sorge ist meiner Ansicht nach nicht Vermeidung, sondern Neugier.
Wenn ein unerfahrener Neuling wie du mit groben Berechnungen ein Gegenbeispiel findet und über Nacht berühmt wird, könnten all diese Mühen und das ganze Gebäude zusammenbrechen; vermutlich waren sie deshalb verärgert.
Wenn ich meinem früheren jungen Ich einen Rat fürs Mathematik-Graduiertenstudium geben würde, dann: Verwende bei jeder nichttrivialen Aufgabe „Beweise X“ mindestens ein Viertel der Zeit auf die Suche nach Gegenbeispielen.
Bei Übungsaufgaben wird das zu 99 % scheitern, aber dein Verständnis des Problems wird viel größer; und im übrigen 1 % kannst du wie ein Genie aussehen.
Sobald man in echte mathematische Forschung einsteigt, verschieben sich diese Wahrscheinlichkeiten deutlich zugunsten eines Ansatzes, der zuerst nach Gegenbeispielen sucht.
Ich erinnere mich, dass mir ein Freund als Student erzählte, jemand habe den ersten Tag eines Seminars hinter sich gebracht, und alle seien begeistert gewesen, weil sie glaubten, er werde Fermats letzten Satz beweisen.
Diese Person war Andrew Wiles; später wurde ein vor der Veröffentlichung entdecktes Problem über mehrere Monate ausgebessert, und schließlich wurde das Ganze publiziert.
Für jemanden, der Mathematik studierte, war das ein unglaublich aufregendes Ereignis; deshalb fühle ich mich wirklich alt, wenn ich die Formulierung „altmodischer Beweis aus den 1990ern“ lese.
Fast die ganze Klasse bestand aus Mathematik-Promovierenden, und ich glaube, ich verstand nicht einmal 20 % des Materials.
Mir gefällt die Stelle, an der Lean etwas von dem Ärgerlichen getan hat, das es manchmal tut: Es beschwerte sich über die menschenübliche Darstellung eines Arguments in der Standardliteratur, und bei näherem Hinsehen stellte sich heraus, dass im menschlichen Argument tatsächlich etwas fehlte.
Abgesehen vom scherzhaften Ärger ist das großartig, und ich denke, Lean und andere Theorem Prover werden künftig wichtige Werkzeuge in der Mathematik sein.
Die Stelle über die mangelhafte Dokumentation moderner Mathematik fühlt sich ähnlich an wie bei UI/UX/Webdesign.
Ein Designer erstellt informelle und ungenaue Mockups, Prototypen und Interaktionsabläufe und übergibt sie an Entwickler; die Entwickler müssen sie dann in Code formalisieren und der Maschine präzise erklären.
Dabei entdecken sie zwangsläufig Lücken wie Interaktionsszenarien oder Codepfade, die im Design nicht berücksichtigt wurden, und manchmal treten große Designfehler zutage, die Entwickler oder Designer schließen müssen.
Design und Entwicklung sind unterschiedliche Rollen und erfordern unterschiedliche Denkweisen, und die meisten Designer wehren sich stark dagegen, wie Entwickler zu arbeiten und zu denken.
Nach diesem Scheitern haben wir gelernt, dass wir Mathematik nicht vollständig formalisieren können; das weist auf ein grundlegendes Problem von Ansätzen hin, die Mathematik mit KI betreiben wollen.
Wenn dich dieses Thema interessiert, lohnt es sich, den tatsächlichen Code anzusehen.
Beispiel: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Auch der Blueprint, der die Gesamtstruktur des Codes erklärt, ist sehenswert: https://imperialcollegelondon.github.io/FLT/blueprint/
Von außen betrachtet ist es sehr interessant zu sehen, wie Lean-Code aussieht und wie Leute dazu beitragen.
Schön ist auch, dass keine Unit Tests nötig sind. In gewissem Sinn ist der abschließende Beweissatz der Unit Test.
Zum Beispiel spielen triviale Beispiele und Gegenbeispiele, mit denen geprüft wird, dass eine Definition nicht leer ist, diese Rolle.
Aus der Perspektive von jemandem, der reine Mathematik betrieben hat, besteht das große Problem darin, dass Mathematiker kaum selbstständige Beweise liefern.
Es gibt keinen Anreiz dazu, und manche Autoren sind sogar stolz darauf, „Details auszulassen“.
Wenn man am Ende einen strengen Beweis will, bei dem man jeden logischen Schritt nachvollziehen kann, muss ein Experte die Lücken füllen, die in der Literatur nicht leicht zu finden sind.
Möglich wird das oft erst, wenn so jemand ein Buch schreibt, das alles erklärt, und manchmal reicht selbst das nicht aus.
Wenn man nur das Aufgezeichnete betrachtet, steht ein großer Teil der modernen Mathematik auf einem instabilen Fundament.
Mathematische Forschungsarbeiten werden für andere Experten des jeweiligen Gebiets geschrieben, und manchmal enthalten sie zu wenige Details, worüber man sich im Peer Review häufig beschwert.
Würde man aber wirklich alle Details liefern, würden die Papers viel länger.
Als Beispiel, das man mit soliden Schulmathematik-Kenntnissen lösen kann, könnte man die Aufgabe nennen, zu beweisen, dass Konstanten C, X > 0 existieren, sodass für gewisse reelle x > X gilt:
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx.Aussagen dieser Form tauchen in der analytischen Zahlentheorie ständig auf und sind für Experten offensichtlich, weshalb sie in Papers fast immer ohne Beweis hingeschrieben werden.
Ein vollständiger, strenger Beweis wäre lang und langweilig, und kein Experte würde ihn lesen wollen.
Diese Haltung hat Trade-off-Kosten, wirkt aber beherrschbar.
Das klingt nach der dritten Stufe, von der Tao spricht: informierte Intuition.
Er sagte: „Wenn man etwas 100-mal gemacht hat, darf man einfach sagen: ‚Wie leicht zu sehen ist‘, und weitermachen.“
Ich habe das so verstanden, dass im Grunde jemand mit einer Datenbank im Kopf herausfinden muss, ob die Voraussetzungen eines Satzes und die Schlussfolgerung des nächsten Satzes zusammenpassen.
Oder gibt es Mathematik, die sich derzeit nicht in einer Form ausdrücken lässt, die ein Proof Checker auswerten kann?
Oder vielleicht ist die Nutzung von Proof Checkern einfach nicht so verbreitet, wie man denkt. Das klingt ähnlich wie die Stellung von statisch typisierten Sprachen in der Programmierung.
Also ob es Fälle gab, in denen ein weithin akzeptierter Beweis wegen eines per Handwinken übergangenen Teils einen fatalen Fehler hatte.
Wenn es solche Fälle nicht gab, kann ich auch verstehen, warum man bei der expliziten Angabe von Details eine lockere Haltung einnimmt.
Ich habe mich immer gefragt, ob die Intuition wirklich stimmt, dass „crystalline cohomology seit den 1970ern so viel verwendet wurde, dass ein Problem längst aufgefallen wäre“.
Ist es wirklich so unmöglich, dass ein ganzes Teilgebiet der Mathematik auf einem fehlerhaften Beweis aufgebaut wird und sich dieses Gebiet dann schlicht als falsch herausstellt?
Er hatte selbst erlebt, wie ein Gebiet durch einen Fehler im „ersten Lemma auf der ersten Seite“ eines grundlegenden Papers zusammenbrach.
Die frühen Arbeiten an UniMath, das Special Year am IAS und das HoTT-Buch haben das Thema der Formalisierung von Mathematik wohl bis zu seiner heutigen Bedeutung vorangebracht.
Wenn das Fundament falsch ist, könnte eines dieser Gegenbeispiele auch den zugrunde liegenden Satz widerlegen; auf einem falschen Fundament weiterzubauen, erhöht also eher die Chance, den Fehler im Fundament aufzudecken.
Ähnlich gilt: Wenn Mathematik gelegentlich angewendet wird, um Vorhersagen zu machen, dann sind bei falscher Mathematik auch die Vorhersagen falsch, und solche falschen Vorhersagen ziehen viel Aufmerksamkeit auf sich.
Eigentlich ist das Wort „Gebiet“ etwas irreführend; viele Theorien sind eher Knoten, die mit vielen anderen Theorien quer durch die Mathematik verflochten sind.
Diese Theorien sind wiederum mit weiteren Theorien verbunden.
Es wäre eine sehr seltsame Situation, wenn nur das Fundament logisch einstürzte, ohne irgendeinen anderen Teil dieses Knotens zu beeinflussen.
Ein riesiger schwebender Block Mathematik, der intern völlig konsistent ist und nur einen einzigen Fehler enthält, ist im Kohomologie-Beispiel dieses Artikels schwer vorstellbar.
Streng genommen ist das eher eine philosophische Haltung, aber ich möchte glauben, dass große Teile der heutigen Mathematik in gewissem Sinne natürlich entdeckt wurden.
Spoiler: Die Welt drehte sich trotzdem weiter.
Seit ungefähr einem Jahr versuche ich immer wieder, Teile eines Analysis-Kurses für Bachelorstudierende über komplexe Analysis in Lean zu formalisieren.
Es gab viel zu lernen und es war lohnend, aber manchmal auch frustrierend.
Erst kürzlich konnte ich die Polarform vollständig als Bijektion von C* nach (-pi,pi] x R definieren, weil ich darauf bestanden hatte, sie „von Grund auf“ zu definieren, obwohl komplexe Zahlen, Potenzreihen, exp und sin bereits in mathlib vorhanden sind.
Ein großer Teil der Schwierigkeiten entstand vermutlich dadurch, dass ich nur einen Bachelor in Mathematik habe, mit Lean/mathlib nicht vertraut bin und niemanden hatte, der mich anleitet. Die Zulip-Community war allerdings sehr hilfreich.
Viele Ergebnisse in mathlib sind ziemlich abstrakt formuliert, sodass schwer zu erkennen ist, wie sie mit den Standardsätzen aus dem Bachelorstudium zusammenhängen oder ob solche Sätze überhaupt in mathlib existieren.
Für die Community der Forschungsmathematik ist das plausibel, für mich persönlich war es aber ein großes Hindernis; wenn Lean stärker in der Lehre eingesetzt wird, könnte das ein ähnliches Problem werden. Mit der Zeit lässt sich das aber wohl aufarbeiten.
Meiner Ansicht nach ist die Beweisautomatisierung noch nicht ausreichend.
Zu vieles ist schwieriger zu beweisen, als es sein sollte, und besonders Typumwandlungen sind mein größter Frustpunkt.
In der gewöhnlichen Mathematik sind die reellen Zahlen eine Teilmenge der komplexen Zahlen; was also für alle komplexen Zahlen gilt, gilt automatisch für alle reellen. In Lean sind es dagegen unterschiedliche Typen, und man muss über injektive Abbildungen/Typumwandlungsoperationen hin- und herwechseln, wodurch der Kern des Beweises aus dem Blick gerät.
Besonders unübersichtlich wird es, wenn sich Typumwandlungen wie von natürlichen Zahlen zu reellen Zahlen und dann weiter zu komplexen Zahlen stapeln.
Natürlich kann das ein themenspezifisches Problem sein; in Bereichen wie der Algebra, wo explizite Abbildungen behandelt werden, wirkt es vermutlich viel natürlicher.
Es ist wirklich einfach, Hinweise zur Nutzung von mathlib zu bekommen: was es gibt und wo es zu finden ist.
Probleme mit übereinander geschichteten Typumwandlungen werden meist durch die Taktik
norm_castgelöst.Selbst wenn es keine konkrete Frage ist, bekommt man oft Vorschläge zu Taktiken, die man nicht kannte, wenn man etwas beiläufig erwähnt oder im Code ein unnötig komplizierter Beweisstil auffällt.
Wenn man nur das Gefühl hat, dass die Formalisierung zu schwierig ist, aber nicht weiß, welche Technik man verwenden sollte, kann man einen mühsam erstellten, unbefriedigenden Beweis als isoliertes Beispiel herausziehen und die Leute fragen, ob sie ihn kürzer machen können.
Solche Fragen werden in der Regel begrüßt, und alle lernen viel dabei.
Dieser Thread scheint davon zu handeln, wie man gute Mathematik schreibt.
Ich habe jahrzehntelang Mathematik gelesen, geschrieben, gelehrt, angewandt und veröffentlicht und außerdem in angewandter Mathematik promoviert.
Es stimmt, dass es beim mathematischen Schreiben Probleme gibt, und manche Mathematik ist miserabel geschrieben.
Es gibt aber auch ziemlich gut geschriebene Mathematik.
Zumindest sollten alle Symbole vor ihrer Verwendung definiert werden; es hilft, vor der Darstellung der Mathematik die Motivation zu geben, und manchmal sind auch intuitive Erklärungen nützlich.
Sorgfältiges Lesen gut geschriebener Mathematik hilft dabei, mathematisches Schreiben zu lernen.
Beispiele sind Paul R. Halmos’ Finite-Dimensional Vector Spaces, R. Creighton Bucks Advanced Calculus, Tom M. Apostols Mathematical Analysis, H. L. Roydens Real Analysis, Walter Rudins Real and Complex Analysis, Leo Breimans Probability und Jacques Neveus Mathematical Foundations of the Calculus of Probability.
Der Autor wollte Fermats letzten Satz genau so verifizieren, wie er in der Literatur entwickelt wurde, und stellte dabei fest, dass ein Lemma, das ein Teilgebiet stützte, in der verwendeten Form nicht wahr ist.
Der Grund, warum er trotzdem glaubt, dass dieses Gebiet im Großen und Ganzen zu retten ist, liegt im Vertrauen darauf, dass jemand bereits ein negatives Ergebnis gefunden hätte, wenn es wirklich falsch wäre.
Nun musste er einen geeigneten Ersatz finden, der dieses Gebiet tragen kann.
Der Autor schreibt ziemlich unterhaltsam; obwohl ich ungefähr die Hälfte nicht verstanden habe, war es leicht zu lesen, was eine merkwürdige Erfahrung war.
Als gutes Wort für den Fall, dass ein Beweis widerlegt wird oder ein Fehler gefunden wurde, habe ich vitiated entdeckt.
Mir gefällt daran, dass es weniger leicht den Irrtum auslöst, die Schlussfolgerung sei als falsch bewiesen worden, aber dennoch ausdrückt, dass der Beweis beschädigt ist und ein neuer Beweis oder eine Reparatur nötig ist.