StartseiteMathlog

Theorema Magnum MMXX: das Liquid Tensor Experiment

Von / 3. März 2022 / 5 Kommentare / Seite 2 von 2 / Auf einer Seite lesen
Mehr

Eine neue Sichtweise auf diese Definition der reellen Zahlen wurde von Dustin Clausen und Peter Scholze in ihrer seit 2018 entwickelten „Verdichteten Mathematik“ aufgebracht. Dezimalbrüche ohne die Identifizierungen der Art 0,999…=1 bilden eine Cantor-Menge, also eine kompakte, total unzusammenhängende Menge. Durch die Identifizierungen wird aus der Cantor-Menge ein Kontinuum.

Clausen und Scholze sind der Überzeugung, dass dieser Zugang der richtige Ansatz zu einem Neuaufbau der Topologie sei. Statt Hausdorffs klassischer Definition topologischer Räume wollen sie Räume – analog zur Konstruktion reeller Zahlen durch Dezimalbrüche – durch Verklebungen total unzusammenhängender Räume gewinnen. Formal definieren sie “verdichtete Mengen” (engl. “condensed sets”) als Garben auf total unzusammenhängenden Räumen (Stone-Räumen). Beispielsweise können sie so die reelle Funktionalanalysis mit Methoden der Zahlentheorie angehen. (Total unzusammenhängende Räume kamen bisher vor allem in der p-adischen Geometrie vor, einem Gebiet der Zahlentheorie.)

Seit dem Ende des 20. Jahrhunderts sind Computerbeweise ein Thema der Mathematik. Dabei gab es einerseits Beweise wie beim Vierfarbenproblem oder der Kepler-Vermutung, wo mit Hilfe eines Computers viele einzelne Fälle abgearbeitet werden konnten, was für Menschen nicht machbar gewesen wäre. Andererseits gab es Formalisierungen bekannter Beweise, die dann mit dem Computer überprüft werden konnten. Der erste war 1986 ein Computerbeweis von Gödels Unvollständigkeitssatz. Es gab dann später auch Formalisierungen der Beweise des Vierfarbenproblem und der Kepler-Vermutung, oder beispielsweise zu Selbergs Beweis des Primzahlsatzes, zum Satz von Feit-Thompson, zum Jordanschen Kurvensatz und zum Brouwerschen Fixpunktsatz.

Das meistverwendete Beweisassistent war zu dieser Zeit HOL Light, basierend auf einer Formulierung der Typentheorie. Vor allem Vladimir Voevodsky vertrat seit 2009, dass man Homotopietypentheorie, basierend auf dem Begriff der Modellkategorie, zur Überprüfung von Beweisen etwa in der Algebra verwenden sollte. Der ursprünglich seit 1989 auf Basis klassischer Typentheorie entwickelte Beweisassistent Coq wurde in diesem Sinne erweitert, konnte aber durchaus auch Sachen, die sich mit Voevodskys univalenter Mathematik nicht machen ließen. Die besten Ergebnisse sollte, wie etwa Kevin Buzzard in Vorträgen ab 2019 vertrat, der auf abhängiger Typentheorie basierende Beweisassistent Lean erreichen.
Als Reaktion auf diese Debatte schlug Peter Scholze in Buzzards Blog 2020 eine Formalisierung seines nach seiner Aussage für die Algebraisierung der Analysis wichtigsten Theorems vor, einem Satz aus seiner Arbeit mit Dustin Clausen über verdichtete Mathematik, der unter dem Namen Liquid Tensor Experiment bekannt wurde und dann von Lean tatsächlich nach nur einem halben Jahr überprüft werden konnte:

Seien 0\textless p^\prime\textless p\leq 1 reelle Zahlen, sei S eine pro-endliche Menge, und sei V ein p-Banach-Raum. Sei \mathcal M_{p'}(S) der Raum der p’-Maße auf S. Dann ist
\mathrm{Ext}^i_{\mathrm{Cond}(\mathrm{Ab})}(\mathcal M_{p'}(S),V)=0 für i\geq 1

Hier noch einmal alle Artikel der Reihe:
Die Klassifikation der einfachen Lie-Algebren.
Der Wiederkehrsatz von Poincaré
Minkowskis Gitterpunktsatz
Ljapunow-Stabilität
Hilberts Nullstellensatz
Der Überdeckungssatz von Heine-Borel
Poincaré-Dualität
Der Primzahlsatz
Hilberts Produktformel
Komponierbarkeit quadratischer Formen
Die Widerspruchsfreiheit der euklidischen Geometrie
Das Runge-Kutta-Verfahren
Lebesgues Satz über dominierte Konvergenz
Fortsetzbarkeit von L-Funktionen
Die Fredholm-Alternative
Der Wohlordnungssatz
Schurs Lemma
Der Spektralsatz für beschränkte Operatoren
Der Satz von Riesz-Fischer
Das Ritz-Verfahren
Borels Gesetz der großen Zahlen
Der algebraische Abschluß von Körpern
Invarianz der Dimension
Der Abbildungssatz
Der Satz vom höchsten Gewicht
Die Klassifikation algebraischer Flächen
Die Einstein-Hilbert-Wirkung
Charakterisierung analytischer Mengen
Multiplikativität der Ramanujanschen Tau-Funktion
Das Noether-Theorem
Kongruenzen der Partitionsfunktion
Der Satz von Thue-Siegel
Das Lokal-Global-Prinzip
Der Banachsche Fixpunktsatz
Die Lefschetzsche Fixpunktformel
Der Fisher-Test
Die Hauptsätze der Werteverteilungstheorie
Der Satz von Peter-Weyl
Das Artinsche Reziprozitätsgesetz
Der Spektralsatz für unbeschränkte Operatoren
Der Satz von Mordell-Weil
Existenz unendlich vieler Geodätischer
Der Ergodensatz
Der Satz von Brauer-Hasse-Noether
Das Fundamentallemma der mathematischen Statistik
Pontrjagin-Dualität
Der Satz von Tichonow
Der Einbettungssatz von Whitney
Der Satz von Winogradow
Der Sobolewsche Einbettungssatz
Der Satz von Teichmüller
Die Riemann-Vermutung für Funktionenkörper
Das Hodge-Theorem
Siegel-Scheiben
Stetiger Funktionalkalkül
Der Satz von Chern-Gauß-Bonnet
Der Eilenberg-Steenrod-Eindeutigkeitssatz
Die Leray-Spektralsequenz
Konditionierung linearer Gleichungssysteme
Das Simplex-Verfahren
Das WKS-Abtasttheorem
Adelische Poisson-Summation
Der Vergleichssatz von Rauch
Die Berechnung des Kobordismusrings
Die Endlichkeit der Homotopiegruppen von Sphären
Der Einbettungssatz von Nash
Serre-Dualität
Die Selbergsche Spurformel
Bott-Periodizität
Der Satz von Grothendieck-Riemann-Roch
Der Eichler-Shimura-Isomorphismus
Der meßbare Riemannsche Abbildungssatz
Der h-Kobordismus-Satz
Der Satz von Feit-Thompson
Der Atiyah-Singer-Indexsatz
Auflösung der Singularitäten
Das Prinzip der großen Abweichungen
Lusins Vermutung
Strukturelle Stabilität hyperbolischer Systeme
Das Yoga der Motive
Konvergente Differenzenschemata der Navier-Stokes-Gleichung
Die Jacquet-Langlands-Korrespondenz
NP-Vollständigkeit des SAT-Problems
Dualität des BMO-Raums zum Hardy-Raum
Die LBB-Bedingung
Die Weil-Vermutungen
Der Superstarrheitssatz
Der Vier-Farben-Satz
Die Calabi-Vermutung
Thurstons Satz über hyperbolische Dehn-Chirurgie
Irrationalität von Zeta(3)
Shelahs Main Gap
Die Kazhdan-Lusztig-Vermutungen
Exotische vierdimensionale Räume
Die Mordell-Vermutung
Der Satz über wandernde Gebiete
Lösung des Wortproblems für hyperbolische Gruppen
Das Gaußsche Klassenzahlproblem
Die Arnold-Vermutung für monotone symplektische Mannigfaltigkeiten
Multiresolutionsanalyse von Wavelets
Der Maßstarrheitssatz
Die Witten-Vermutung
Das eingeschränkte Burnside-Problem
Monströser Mondschein
Mirrorsymmetrie für Calabi-Yau-Hyperflächen in torischen Varietäten
Die Thom-Vermutung
Der große Satz von Fermat
Die Milnor-Vermutung
Das Scheffer-Shnirelman-Paradoxon
Die Baum-Connes-Vermutung für kokompakte Gitter in SL(3)
Vergleich der Regulatoren von Beilinson und Borel
Das Skalierungslimit schleifenbereinigter Irrfahrten
Die Langlands-Korrespondenz für Funktionenkörper
Die Gromov-Witten-Invarianten der projektiven Gerade
Die Poincaré-Vermutung
Der Satz von Green-Tao
Die Mirzakhani-McShane-Identitäten
Die Arnold-Vermutung
Serres Modularitätsvermutung
Das Fundamentallemma
Nichtlineare Landau-Dämpfung
Eindeutige Quantenergodizität für SL(2,Z)\H
Die Read-Vermutung
Die Waldhausen-Vermutung
Der Satz über beschränkte Primzahllücken
Die Grunewald-Ash-Vermutung
Die Yau-Tian-Donaldson-Vermutung
Erdős’ Diskrepanz-Problem
Optimalität der E8-Kugelpackung
Die Hodge-Riemann-Relationen für Matroide
Die Onsager-Vermutung
Das Liquid Tensor Experiment

1 / 2
Stichworte: , ,
Mehr

Kommentare (5)

  1. #1 Bernd Nowotnick
    4. März 2022

    Zu „Für metrische Räume definieren die offenen Mengen (also diejenigen, wo zu jedem Punkt eine offene metrische Kugel um den Punkt noch in der Menge liegt) eine solche Topologie…Zur Mengenlehre im damaligen Verständnis zählten auch die Theorie der Punktmengen und die Maß- und Integrationstheorie“:
    Eine relative Bewegung verschmiert die Mitten zweier Massen. Stellen wir uns vor auf der Richtung x befinden sich ein Atomkern und ein Elektron in Resonanz. Da es aber drei Orts- und drei Geschwindigkeitskoordinaten gibt sind die Orte und die Geschwindigkeiten in einem sechsdimensionalen abstrakten Raum aufgespannt. Da aber die Mittelpunkte sich nur in eine Raumrichtung vor und zurück bewegen können, kann man den Phasenraum weitaus unkomplizierter gestalten. Man braucht bloß die Geschwindigkeiten der Mittelpunkte zu betrachten. So lässt sich der Phasenraum durch ein gewöhnliches kartesisches Koordinatensystem darstellen, wobei die x1-Achse der Geschwindigkeit des Atomkerns und die x2-Achse der Geschwindigkeit des Elektrons entsprechen. Ein beliebiger Punkt in dem Koordinatensystem gibt also die Geschwindigkeit und je nach Vorzeichen die Richtung der beiden Mittelpunkte an. Doch nicht alle Werte sind möglich. Zum Beispiel ist der Atomkern immer langsamer wie das Elektron. Um herauszufinden, welche Geschwindigkeitskombinationen erlaubt sind, braucht man die Energie- und die Impulserhaltung, denn die Energie und der Impuls vor und nach einem Wechsel der Bewegungsrichtung bleiben im gesamten System immer gleich. Die Bewegungsenergie des Atomkerns und des Elektrons auf x ist konstant. Indem man die Achsen des Koordinatensystems passend wählt nimmt diese Formel die Gestalt einer Gleichung für einen Kreis v1^2 + v2^2 = konstant an, so das zu jedem Zeitpunkt die Geschwindigkeiten der beiden Mittelpunkte einen Wert auf dem Kreis im Phasenraum haben. Die irrationale Zahl π steckt in der runden Geometrie des Phasenraums, wodurch die Bogenlängen, die benachbarte Punkte auf dem Kreis einschließen, immer gleich groß sind. Wenn also N die Anzahl der elastischen Stöße bezeichnet, L die Bogenlänge und r den Radius des Kreises, dann ergibt sich die Ungleichung: N · L · r ≤ 2π r. Da N auf x die Nachkommastellen von Pi bei N · √(m/M) ≤ π fordert muss der Wert von √(m/M) Werte wie 1/10, 1/100, 1/1000 und so weiter annehmen was immer dann der Fall ist wenn das Massenverhältnis 1 : 100n beträgt. Weil der Radius auf beiden Seiten auftaucht kann man ihn wegstreichen. Bei so einem Aufbau mit zwei Massen m und 100^n · m finden stets 10^n*π Stöße statt und das ist immer dann der Fall wenn das Massenverhältnis 1 : 100^n beträgt. Meiner Meinung nach laufen die ungestörten Planetenbahnen über die Anpassung des Drehwinkels nach diesem Prinzip, wie dann auch die Magnetfelder von Sternen da hinein wirken, wobei die kleinste Menge auf x das Wirkungsquantum der Bewegung von einer ganzen Zahl zur nächsten ganzen Zahl ist.

  2. #2 Johan Commelin
    5. März 2022

    The Liquid Tensor Experiment is not yet complete. In half a year, we completed the formal verification of the main technical ingredient. We are currently working on the second stage of the project. See https://leanprover-community.github.io/liquid/dep_graph_section_2.html for an overview of the remaining work.

  3. #3 Thilo
    5. März 2022

    Thank you for the information.

  4. #4 Thilo
    5. März 2022

    Einen ausführlicheren Artikel hat das Quanta Magazine: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

  5. #5 Formalisierung der Mathematik – wann führen Computer die Beweise? – Mathlog
    7. Mai 2022

    […] und der Professor für Wissensrepräsentation Michael Kohlhase. Scholze erzählt, dass er durch das Liquid Tensor Experiment nicht nur Sicherheit über die Korrektheit, sondern auch ein besseres Verständnis des Beweises […]