Mathematiker nehmen den 350 Jahre alten Problembrocken „Fermats letzter Satz“ mit einem Computerbeweis in Angriff

Fermats letzter Satz wird in einer Computersprache neu bewiesen

• Professor Kevin Buzzard vom Imperial College London will ab Oktober 2024 einen formalen Beweis von Fermats letztem Satz (FLT) mit dem Theorembeweiser Lean schreiben.
• Der britische Engineering and Physical Sciences Research Council[EPSRC] hat beschlossen, Professor Buzzard ab diesem Monat fünf Jahre lang mit Forschungsgeldern zu unterstützen.
• Ein mit dem plasTeX-Plugin Lean blueprints erstellter Projektplan soll Ende April 2024 veröffentlicht werden.

Ist Fermats letzter Satz nicht bereits bewiesen?

Doch, das ist er. Der britische Mathematiker Andrew Wiles veröffentlichte den Beweis 1994, und 1995 wurde er offiziell publiziert. Ein formaler Beweis, der in der Sprache eines interaktiven Theorembeweisers[ITP] geschrieben ist, existiert jedoch noch nicht.

Interaktiver Theorembeweiser? Formaler Beweis? Was ist das?

• Interaktiver Theorembeweiser[ITP]: Ein Computerprogramm, das Menschen beim Schreiben formaler Beweise hilft. Wird auch Proof Assistant genannt.
• Formaler Beweis: Ein Beweis, der von einem Computerprogramm namens Proof Verifier überprüft werden kann. Proof Assistants übernehmen in der Regel auch die Rolle eines Proof Verifiers.

Sind Theorembeweiser künstliche Intelligenz?

Bei neuronalen Theorembeweisern[NTP] kann man das so sehen, aber viele interaktive Theorembeweiser einschließlich Lean basieren nicht auf Machine Learning.

Stell Lean bitte vor.

• Interaktiver Theorembeweiser und zugleich rein funktionale Programmiersprache.
• Basiert auf der Theorie abhängiger Typen.
• Verfügt über Funktionen wie Type Classes, erweiterbare Syntax, Makros und Metaprogrammierung.
• Im Vergleich zu anderen Proof Assistants hat Lean unter seinen Nutzern besonders viele Mathematiker, die außerhalb der mathematischen Grundlagenforschung arbeiten.

Warum will man einen formalen Beweis von Fermats letztem Satz schreiben?

Um Professor Kevin Buzzard in einem Post auf X zu zitieren: „Damit wir dem Computer moderne Zahlentheorie beibringen können, um schließlich Zahlentheoretikern helfen zu können.“

Links

• Nachricht von Professor Kevin Buzzard im Lean-Zulip-Chat vom 3. Oktober 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
• Lean-Mathematikbibliothek: https://github.com/leanprover-community/mathlib4
• New-Scientist-Artikel: https://institutions.newscientist.com/article/…
• Popular-Mechanics-Artikel: https://popularmechanics.com/science/math/…

[calofmijuck]

Ich drücke die Daumen. Wer sich für Formal Proof interessiert, dem empfehle ich auch die Vorlesung Machine Assisted Proofs von Professor Terrence Tao (https://www.youtube.com/watch?v=AayZuuDDKP0).