In der Mathematik gibt es ein Gespenst

• Lean ist eine Programmiersprache, die für die Formalisierung von Mathematik entwickelt wurde und es Mathematiker:innen ermöglicht, mathematische Sätze wie Code zu behandeln.
• Nutzer schreiben Satz, Beweis, Axiom etc. in Codeform; der Beweisablauf wird über ein Befehlsset namens tactic durchgeführt.
• Ein Beweis muss nicht vollständig fertiggestellt sein, er kann aber mit sorry vorläufig abgeschlossen werden; das ist jedoch ein falscher Beweis ähnlich any in TypeScript.
• Wird ein falsches Axiom hinzugefügt (z. B. 2 = 3), entsteht das Risiko eines logischen Widerspruchs und der Beweisbarkeit jeder Behauptung.
• Lean leitet Schlussfolgerungen nur aus den logisch ausgewählten Axiomen und dem Beweissystem ab, daher hat die Aufrechterhaltung mathematischer Gültigkeit große Bedeutung.

---

Lean: Mathematik als Code behandeln

• Lean ist eine Programmiersprache, die auf formalisiertes Mathematikschreiben spezialisiert ist.
• Mit Lean können Mathematiker mathematische Sätze und Beweise in Codeform ausdrücken und so strukturieren, dass sie kooperativ geteilt werden können.
• Es entwirft eine mögliche Zukunft, in der ein Großteil des mathematischen Wissens in Codeform vorliegt und mechanisch verifiziert sowie kombinierbar wird.

Der erste Schritt eines Lean-Beweises

• In Lean ist eine einfache Theorem-Deklaration der Form theorem two_eq_two : 2 = 2 := by sorry möglich.
• Wenn ein Beweis unvollständig ist, kann sorry verwendet werden, aber das ist nur ein vorläufiger Schritt, kein echter Beweis.
  • sorry lässt die Beweisprüfung von Lean passieren, ist jedoch logisch nicht vertrauenswürdig.
• Für vollständige Beweise wird eine Taktik wie rfl (Reflexivität) verwendet, um offensichtliche Gleichungen wie 2 = 2 zu beweisen.
• Bereits bewiesene Inhalte können mit exact usw. in anderen Theoremen wiederverwendet werden, was die Modularität betont.

Axiome und Widerspruch: Wenn die Mathematik von einem Gespenst heimgesucht wird

• Wenn ein Axiom wie axiom math_is_haunted : 2 = 3 hinzugefügt wird, betrachtet Lean dies als wahr.
• Dieses Axiom kann anschließend im Beweisprozess verwendet werden und sogar mathematisch unsinnige Schlussfolgerungen (z. B. 2 + 2 = 6) werden beweisbar.
• Es ist möglich, mit der Tactic rewrite 2 durch 3 zu ersetzen und den Beweis mit rfl abzuschließen.
• Wenn ein ungeeignetes Axiom zu einem Widerspruch führt, kann in Lean der Zustand eintreten, dass jede Aussage beweisbar ist (logischer Kollaps).
• Tatsächlich führte etwa Russells Paradoxon zu Beginn des 20. Jahrhunderts dazu, dass Inkonsistenzen in Axiomensystemen zu einer grundlegenden Fragestellung der Mathematik wurden.
• So zeigt Lean eindrücklich, dass die Wahl der Axiome entscheidend für die Aufrechterhaltung der logischen Konsistenz eines Systems ist.

Lean als Beweisprüfer

• Sind die Axiome gut gewählt und Lean ist logisch korrekt, liefert es theoretisch verlässliche Schlüsse.
• Von einfachen Gleichungen bis zu sehr komplexen Sätzen (z. B. Fermat's Last Theorem) werden alle nach denselben Prinzipien geprüft.
• Bei großen Theoremen entsteht der vollständige Beweisbaum durch wiederholtes, aufeinander aufbauendes Beweisen von Unterstrukturen und Sätzen.
• Als Beispiel wird ein großes Projekt beschrieben, das Fermat's Last Theorem in Lean formalisiert, mit dem Ziel, dass am Ende ein vollständiges Beweissystem ohne sorry steht.

Die Freude am Lernen von Lean

• Das Beweisen in Lean ist eine kreative Verbindung von Programmierung und Mathematik.
• Anfangs geht es darum, einfache Aussagen zu beweisen; allmählich wird der Prozess, schrittweise immer komplexere und tiefere Mathematik rigoros aufzubauen, zur eigentlichen Freude.
• Offizielle Tutorials und Community-Materialien (z. B. Natural Numbers Game, Mathematics in Lean usw.) eignen sich gut für den Einstieg.
• Mit Lean formalisierst du die Logik direkt selbst und entdeckst die Schönheit hinter raffinierten Ideen und Argumenten erneut.
• Das Fazit lautet: Für manche Menschen macht Lean einfach besonderen Spaß, auch ohne äußeren Anlass.

[GN⁺]

Hacker-News-Kommentare

• Ich denke in letzter Zeit über die Idee nach, Nachrichten oder Sachartikel mit einem System wie Lean – oder mit Lean selbst – neu zu schreiben, indem man jede Aussage als Theorem behandelt, das bewiesen werden muss, und Belege als Teil des Beweises einbindet. Man könnte zum Beispiel zusammengesetzte Beweise verwenden wie: „Wenn drei von mir genehmigte Quellen behaupten, dass etwas wahr ist, dann gilt es als wahr.“ Außerdem müsste es möglich sein, das gesamte Dokument so zu markieren, dass man „bewiesene“ Behauptungen hervorgehoben sehen kann. Es wäre nicht perfekt, aber ein Versuch, die Strenge, die die Medien früher einmal boten, technisch neu umzusetzen.
  • Die Formalisierung natürlichsprachlicher Aussagen ist ein Gebiet voller Hürden, aus ähnlichen Gründen, aus denen es schwer ist, Code zu schreiben, der mit der realen Welt interagiert. All die Konzepte, die wir als selbstverständlich ansehen – Identität, Zeit, Kausalität usw. – müssen innerhalb des Formalismus fein granular behandelt werden, damit sich Fakten überhaupt verknüpfen oder ausdrücken lassen. Trotzdem ist das ein wirklich spannendes Problem. OpenCog war ein Projekt, das diesen Bereich konsequent verfolgt hat, und auch das Forschungsfeld Wissensrepräsentation und Schlussfolgern (KRR) existiert in der Wissenschaft eigenständig. Das IJCAI-Journal ist voll von solcher Forschung, und Philosophinnen und Philosophen haben viele Logiken entwickelt, um Argumentationen über Zeit, Modalität, Wahrscheinlichkeit usw. zu formalisieren. Leider lassen sich diese nicht ohne Weiteres miteinander kombinieren, sofern das nicht inzwischen gelöst wurde.
  • Ich denke, die wichtigsten Überzeugungen, die wir bei Nachrichten haben sollten, lassen sich meist nicht als Sammlung absoluter Aussagen beweisen. Werkzeuge, die Schlussfolgerungsketten berechnen, etwa bayessche Wahrscheinlichkeiten, scheinen dafür geeigneter zu sein. Ich habe schon Tools für numerische Schätzungen dieser Art gesehen.
  • Ich habe die Erfahrung gemacht, dass sich mein Sachschreiben stark verbessert hat, nachdem ich an der Uni Mathematik gehört hatte. Wenn ich Essays meiner SO (Partnerin) und meiner jüngeren Schwester las, habe ich Strenge angelegt, als würde ich einen logischen Beweis prüfen: „Hier wird behauptet, C folge aus B, aber es fehlt eigentlich der Grund, warum B aus A folgt; also kann man nicht sagen, dass C aus A folgt.“ Mit Tools wie LLMs scheint es zwar möglich, daraus ein Programm zu machen, aber Halluzinationen – also das Erzeugen nicht vorhandener Behauptungen – setzen dem klare Grenzen.
  • Man muss vorsichtig sein: So ein Ansatz kann sehr leicht selbst radikalen oder unsinnigen Behauptungen eine Aura logischer Objektivität verleihen. Ein Blick auf die politischen Ansichten von Gottlob Frege, einem der Väter der modernen Logik, könnte als Warnung dienen passender Link
  • Ich fände es interessanter, die gesamte Argumentationsstruktur zu einem bestimmten Thema als Karte zu zeichnen. Man beginnt zum Beispiel mit einer großen Frage wie „Existiert Gott?“, entfaltet dann hierarchisch die Argumente dafür und dagegen, deren Gegenargumente und wiederum deren Erwiderungen. Zitate wie „Platon hat ein solches Argument vorgebracht“ würden dabei nicht als Belege dienen, sondern eher historischen Kontext liefern. Entscheidend wäre nicht, einen Sieger zu küren, sondern eine Argumentationskarte zu erstellen, damit man nicht ständig um dieselben Punkte kreist.
• Ich frage mich, ob wir am Ende ein Wörterbuch von Beweisen aus einigen wenigen selbstverständlichen Wahrheiten aufbauen, auf dem sich dann allerlei weitere Beweise logisch aufschichten. Zusätzliche Beweise wären dann einfach logische Kombinationen bereits vorhandener Beweise. Ich wünschte, daraus würde ein Spiel im Stil von Zachtronics gemacht! Ein Spiel namens Euclidea vermittelt in der Trigonometrie ein ähnliches Gefühl; dieses Konzept, einen Turm aus Logik zu bauen, ist einfach unglaublich reizvoll. Ich frage mich, ob reine Mathematik genau das ist, ob Professorinnen und Professoren für reine Mathematik gerade darin ihre Freude finden, dieses Logikwörterbuch zu erweitern, und ich meine mich zu erinnern, dass es von einem berühmten Mathematiker eine Liste grundlegender Beweise gab – wenn jemand weiß, wer oder was das war und wie es heißt, wäre das toll. Vermutlich sind das Axiome.
  • Es gibt bereits ein passendes Spiel, auch wenn es vielleicht nicht ganz dem entspricht, was du suchst (und es ist kein Spiel, in dem man die gesamte Mathematik baut). Ich habe es tatsächlich gespielt, und es hat ziemlich viel Spaß gemacht. Das im Artikel erwähnte leanprover-community/nng4 ist genau so ein Beispiel.
  • Zur Aussage „Bitte macht daraus ein Spiel im Zachtronics-Stil“: Man könnte sagen, Mathematik ist genau dieses Spiel, wenn auch halb im Scherz. Ich denke aber, eine Spielversion wäre wirklich sehr unterhaltsam. Reine Mathematik ist im Kern genau so ein System; im Grundstudium fühlt es sich definitiv so an, bei Forschung auf Paper-Niveau dann etwas weniger. Wenn du dieses Spielgefühl suchst, würde ich empfehlen, ein Lehrbuch zur abstrakten Algebra wie Dummit and Foote anzuschauen. Beweise haben dort etwas Spielerisches, und für bekannte Bücher findet man online auch Erklärungen, wenn man feststeckt.
  • Vielleicht meinst du Euklids Axiome – ein System, in dem Konzepte wie Punkt, Gerade, Ebene und Parallele definiert sind. Auf einer Kugel statt auf einer Ebene bricht dieses System zusammen. Oder du meinst die Zermelo-Fraenkel-Mengenlehre (ZF/ZFC), auf der die moderne Mathematik insgesamt aufgebaut ist.
  • Es gibt auch ein Spiel namens Bombe, eine Variante von Minesweeper. Anstatt Zellen direkt zu öffnen, erstellt man Regeln dafür, „wann man eine Flagge setzen darf“. Mit steigender Schwierigkeit verketten sich diese Regeln wie Lemmata, und wenn die Fähigkeiten des Spielers wachsen, lassen sich die Beschränkungen des Werkzeugkastens lockern und verallgemeinern Spiel-Link
  • Mathematik ist im Wesentlichen der Prozess, aus Axiomen ausgehend Schlussfolgerungen herzuleiten. Natürlich ist das nicht alles, aber auf meinem Niveau verstehe ich es so.
• Ein bisschen kleinlich vielleicht, aber es ist seltsam zu sagen, das Theorem two_eq_two sehe wie eine Funktion aus. Es hat ja keine Argumente und ist daher eher eine Konstante, auch wenn ich natürlich verstehe, dass Konstanten letztlich Funktionen ohne Argumente sind. Überzeugender wäre vielleicht, x_eq_x wie unten zu verwenden und es in 2_eq_2 tatsächlich wie eine Funktion anzuwenden.

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Hier sieht x_eq_x wie eine Funktion aus und wird in 2_eq_2 auch tatsächlich so verwendet.
  • Guter Punkt! Ich habe es nicht so gemacht, weil mir Leans Umgang mit Argumenten – besonders Konzepte wie dependent types, bei denen man für x einen Beweis von x = x zurückbekommt – selbst noch etwas fremd ist und ein eigenes Thema verdient. Das werde ich im nächsten Artikel behandeln.
• Eine Schwierigkeit beim Lernen von Lean ist für mich, dass Tactics (rfl und ähnliche) zu umfassend sind und man selbst mit Tutorials ihre genaue Bedeutung nur schwer erfassen kann. Bei C kann ich Zustandsänderungen bis auf Bit-Ebene verfolgen, aber Lean wirkt irgendwie unbestimmt. Auch die Syntax der rewrite- (rw-)Tactic fühlt sich für mich unnatürlich an.
  • Auch in Coq (jetzt Rocq) fand ich die Eingewöhnung an Tactics immer schwer. Ich hatte zum Beispiel einmal A = B und P(A,A) und wollte zu P(A,B) kommen, aber rewrite funktionierte aus schwer erklärbaren Gründen nicht – vermutlich wegen der Definition einer Zwischenstruktur. Metamath und die set.mm-Datenbank hingegen verzichten ganz auf Tactics und lassen nur konkretes Schlussfolgern zu, also etwa nur Inferenzregeln wie ax-mp. Das hat aber wiederum den Nachteil, dass man sich eine ganze Menge nützlicher Hilfslemmata merken muss.
  • Das ist einer der Gründe, warum ich Agda bevorzuge. Agda hat praktisch kaum Tactics; stattdessen schreibt man mit der Curry-Howard correspondence die Beweisterme direkt in einer funktionalen Programmiersprache. Wenn man dort allerdings bei Abstraktion und Funktionsbildung nachlässig ist, werden selbst triviale Dinge absurd mühsam – Disziplin ist also wichtig.
  • Zumindest in Lean kann man sich die Definition von Tactics über „go to definition“ ansehen und so nachvollziehen, wie sie intern funktionieren. Beim Lernen ist das wegen der Menge zwar überwältigend, aber letztlich ist alles einsehbar – auch wenn man bei der grundlegenden Typentheorie irgendwann den Faden verlieren kann. Und weil du sagst, die rewrite-Syntax wirke unnatürlich: Mich würde interessieren, was für dich eine natürliche rewrite-Syntax wäre.
  • Interessant fand ich, dass Tactics komplett „User-Level“-Code sind und außerhalb des Beweis-Kernels liegen. Das ergibt Sinn, weil man den kleinen, verifizierten Kernel möglichst unverändert lassen will. Es bedeutet aber auch, dass bestehende Beweise bei Versionsupdates oder Änderungen an Tactics kaputtgehen könnten. Ich frage mich, wie groß dieses Problem in der Praxis tatsächlich ist.
  • Entgegen meiner Erwartung dachte ich, dass in Lean Reflection und rewrite fundamentaler wären als Addition. Lean scheint Addition eingebaut zu haben, aber rfl oder rewrite muss man offenbar jedes Mal explizit anwenden. Vielleicht gibt es in Lean eine Art Prelude, das das automatisch übernimmt.
• Ich frage mich, ob es in Lean eine Möglichkeit gibt, Beweise nicht-interaktiv zu lesen. Beim natural number game bestehen die Beweise gefühlt nur aus Listen von Befehlen wie rw [x], und ich finde sie so sehr schwer lesbar. Im Editor kann ich den Zustand jeder Zeile sehen, aber dafür muss ich ständig klicken, was den Fluss unterbricht. Bei Python wäre es genauso, wenn es keine Einrückung gäbe und man die Struktur eines Blocks nur durch Anklicken verstehen könnte. Vielleicht liegt das aus meiner Sicht an den eingeschränkten Befehlen am Anfang des Spiels, aber ich frage mich, ob sich dieser Lesefluss in einer echten, vollständigen Lean-Umgebung verbessert.

  • Gibt es in Lean eine Möglichkeit, Beweise nicht-interaktiv zu lesen?
    Ich habe das vor Kurzem selbst nachgeschlagen. Der lean-in-latex-Blog zeigt eine Möglichkeit, diesen Fluss auch außerhalb des Editors und ohne Klicken nachzuvollziehen, und man bekommt ein Gefühl dafür, wie die Lean-Community an so etwas herangeht.

  • In Rocq gab es früher einmal eine „mathematische Beweissprache“. Konkrete Nutzungsbeispiele sind schwer zu finden, aber sie sah ungefähr so aus:

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    So ein Ansatz ließ sich eher wie ein „handgeschriebener Beweis“ in einem Paper lesen, wurde aber kaum benutzt und verschwand deshalb wieder. Ähnlich ist Isabelles Isar-Proof-Sprache, die sogar eher dem Standardansatz entspricht, zum Beispiel:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Dabei werden die gesamte logische Struktur und Zwischenergebnisse explizit notiert, und nur dort, wo Details wichtig sind, kann man Tactics mit by ... abkürzen. Ich weiß nicht, ob Lean etwas Vergleichbares hat, aber zumindest taugt das als Suchbegriff oder als Frage für ein Lean-Forum.
  • Wirklich eine gute Frage! Ich bin noch Anfänger, also nimm das nicht als endgültig verlässlich, aber ich teile gern meinen Eindruck. Nach ein paar Monaten mit Lean habe ich gemerkt, dass das Lesen von Beweiscode anders ist als das Lesen von Programmcode; es fühlt sich eher wie „Scannen“ an. Man achtet auf die grobe Argumentationsstruktur, darauf, welche Tactics verwendet werden und welche Lemmata zum Einsatz kommen. Der tatsächliche Lean-Code-Stil arbeitet mit Einrückung bei jedem neuen Goal und Ausrückung, wenn ein Goal abgeschlossen ist. Deshalb liest man stark über die „Form“ des Arguments; siehe zum Beispiel mein PR-Beispiel. Wenn man sich an Tactics gewöhnt, erkennt man etwa, dass intro den Eintritt in einen Quantor bedeutet oder constructor ein Goal aufteilt. Im Grunde sind Tactics Makros oder eine DSL, die einen Beweisbaum beziehungsweise Termbaum erzeugen. Beim Lesen fühlt es sich für mich an wie das Manipulieren eines Baums – Teile zerlegen, Reihenfolge füllen usw. Trotzdem bleibt es dabei, dass man klicken muss, wenn man Zwischenaussagen im Beweis ganz genau sehen will. Beweise mit einer guten Idee lassen sich jedoch ähnlich klar lesen wie die logische Entwicklung in einem Paper. Wer also Absicht klar vermitteln will, schreibt gut lesbare Namen, eine klare Entwicklung, zieht kleine Lemmata heraus und notiert erst die Hypothesen, bevor ein kurzes Stück Beweiscode folgt. Umgekehrt wird das, was mathematisch offensichtlich, maschinell aber lästig ist, oft „gegolft“, also auf möglichst kurze Schreibweise gebracht. Dieser Golf-Stil macht den Code häufig kürzer, behandelt dann aber genau die Teile, die für Menschen ohnehin intuitiv sind. Kurz gesagt: Die Struktur beim Lesen von Lean ist implizit, aber man kann sie klarer machen, und je vertrauter man mit Tactics wird, desto besser erkennt man die Struktur auch ohne Klicken. Oft reicht schon ein Blick auf die Lemma-Namen, um den großen Fluss zu verstehen, und die Reihenfolge lässt sich leicht rekonstruieren.
• Der Inhalt war wirklich großartig. Ich denke, es gibt nur wenige Menschen, die so etwas in einer so leicht verdaulichen Form erklären können. Das Geheimnis ist, all die kleinen Schritte zu zeigen, die Expertinnen und Experten sonst einfach überspringen.
  • Danke!
• Mich würde interessieren, ob ich in diesem Thread Meinungen zur Zukunft von Lean im Vergleich zu Idris/Coq/Agda hören könnte. Ich möchte Wissensrepräsentation lernen, habe aber Bedenken wegen Community-Größe und Zukunftsrisiken, bevor ich mich tief in irgendetwas einarbeite. Früher habe ich einmal Zeit in clojure core.logic investiert und mich dann an der geringen Aufmerksamkeit und der kleinen Community verbrannt; deshalb tue ich mich schwer, einfach loszulegen.
  • Aus meiner praktischen Erfahrung werden Lean und Coq/Rocq deutlich mehr verwendet als Idris oder Agda, und sie haben auch größere Bibliotheken und Communities. Rocq wird häufig für Programmverifikation genutzt, was vermutlich auch an seiner längeren Geschichte liegt; es hat einige Eigenheiten, und Lean könnte es dort möglicherweise bald einholen. Lean wird am häufigsten für mathematische Theorembeweise verwendet. Bekannte Rocq-Projekte sind CompCert, CertiCoq und sel4; es gibt auch Anwendungen in der Verifikation realer Flugzeugsoftware (siehe diese kuratierte Projektliste). In Lean gibt es große Projekte wie mathlib (eine Sammlung mathematischer Beweise), den Beweis des letzten Satzes von Fermat (FLT proof project) und PFR. Soweit ich weiß, haben Idris und Agda keine wirklichen „Real-World“-Projekte, aber da könnte ich mich irren. Natürlich sind alle diese Communities winzig im Vergleich zu Sprachen oder Communities wie C++ oder JavaScript, und echte Programmverifikation ist in der Praxis sehr langsam und unerquicklich. Vielleicht bringt die Weiterentwicklung von KI irgendwann einen grundlegenden Wandel, aber die Fähigkeiten, die man dabei lernt, bleiben trotzdem nützlich.
  • Ich glaube ehrlich gesagt nicht, dass man auf dieses Feld „wetten“ sollte. Die meisten Mathematikerinnen und Mathematiker haben an Formalisierung kaum großes Interesse, weil die Kluft zwischen handgeschriebenen Beweisen und der strengen Syntax, die Computer verlangen, sehr groß ist. Man sollte also eher mit Freude am Lernen und Ausprobieren herangehen. Was die Zukunftsaussichten angeht, wirkt Lean in letzter Zeit zwar am aktivsten, aber alle haben ältere Nutzergruppen, und ich würde mich mit Prognosen zurückhalten.
• Ich frage mich, ob man auch ohne besondere Tricks oder Kniffe interessante Entdeckungen machen könnte, indem man einfach zufällig irgendetwas in Lean wirft und schaut, ob Lean es akzeptiert. Oder könnte man so etwas mit einem automatisierten System oder einem LLM laufen lassen, das massenhaft obskure Beweise oder Theorien ausprobiert und dann nur den Erfolg oder Misserfolg auswertet? Die Frage mag unbeholfen sein; ich verstehe gerade so eben Prolog.
  • Aus Sicht von jemandem, der beruflich certified programming macht, sind generative KI und formale Methoden eine Traumkombination. Ob LLMs Programmierer irgendwann ersetzen, hängt meiner Meinung nach stark davon ab, wie gut KI mit certified programming und kombinatorischem Schließen wird.

    Führt zufälliges Herumprobieren zu interessanten Entdeckungen?
    Frühere KI funktionierte gut bei Problemen mit kleinem Zustandsraum wie Dame. Schach ist etwas schwieriger, und Go ist mit traditioneller KI praktisch unmöglich, wenn man kein Machine Learning einsetzt. Formale Sprachen haben einen unvorstellbar großen Zustandsraum und eine riesige Zahl durchsuchbarer Zustände. Wenn die Natur des Problems klar genug ist, kann man mit SMT-Solvern brute force vorgehen. Ursprünglich gehören SMT-Solver und Proof Assistants zu verschiedenen Teilgebieten formaler Methoden, aber inzwischen ergänzen sie sich zunehmend gut (siehe Sledgehammer und Lean-SMT).
    Was, wenn man LLMs oder automatische Systeme beliebige Beweise oder Theorien ausprobieren lässt?
    Das ist zwar noch kein Mainstream-Thema, aber es wird intensiv erforscht und erprobt. Schon vor dem LLM-Boom gab es dafür jahrelang große Fördermittel, etwa für frühere Arbeiten wie „Learning to Find Proofs and Theorems by Learning to Refine Search Strategies“, und neuere Forschung wie DeepSeek-Prover gibt es ebenfalls. Wie man solche Systeme trainiert und wie weit ihre Zukunftschancen reichen, ist noch völlig offen.
    Gegenwärtige LLMs sind in Rocq- und Lean-Sprachen noch recht schwach, und wenn sie etwas Falsches ausgeben, ist die Korrektur äußerst schmerzhaft. Trotzdem erwarte ich, dass das Niveau von KI-Tools mit der Zeit deutlich steigen wird.

  • Das ist tatsächlich ein sehr aktives Forschungs- und Experimentierfeld!
    Die Lean-Community versammelt sich stark auf Zulip, und im Machine-Learning-for-Theorem-Proving-Kanal findet man viele relevante Threads und Referenzen.
• Ich bin durch alphaproof überhaupt erst auf Lean aufmerksam geworden, und dieser Einführungstext war großartig. Könntest du vielleicht erzählen, womit du in Lean gerade arbeitest?
  • Im Moment lerne ich mit Lean einfach Mathematik, konkret indem ich Taos Lean-Lehrmaterial durcharbeite und in den Übungen die offenen sorry-Stellen selbst ausfülle (meine Lösungen sind hier).
• Ich frage mich, ob es in Lean einen Prüfmodus gibt, der automatisch verhindert, dass unzuverlässige Beweise (proof with "sorry") oder zusätzliche Axiome hineingeraten. Kann man zum Beispiel überprüfen, dass „ein Beweis in keiner Weise sorry verwendet“ oder dass er „nur von einer festen Axiomenmenge an Beweiskraft abhängt“?
  • Das im späteren Teil des Artikels erwähnte #print axioms some_theorem dürfte doch genau dafür ein Beispiel sein. Damit lässt sich sehen, ob ein Beweis direkt oder indirekt von sorry oder von ungeprüften Axiomen abhängt.
  • Mit print axioms kann man prüfen, ob zusätzliche Axiome eingeführt wurden. Außerdem kann man darauf achten, ob der Code ohne Warnungen oder Fehler kompiliert. Das Utility SafeVerify fängt auch einige Tricks ab, die RL-Systeme gefunden haben.
  • Dass das auch per Makro möglich ist, wird hier beschrieben.