Warum nicht einfach Lean verwenden?

 (lawrencecpaulson.github.io)
1 Punkte von GN⁺ 1 일 전 | 1 Kommentare | Auf WhatsApp teilen
  • Die Geschichte der Formalisierung von Mathematik begann nicht mit Lean; vielmehr haben Systeme aus mehreren Traditionslinien seit fast 60 Jahren zentrale Techniken und Ergebnisse angesammelt
  • Werkzeuge wie AUTOMATH von 1968, die LCF-Familie, HOL, Rocq, ACL2 und Mizar haben ein breites Spektrum an Formalisierungen hervorgebracht, von der reellen Analysis über den Primzahlsatz und den Vierfarbensatz bis hin zur Kepler-Vermutung
  • Lean hat auf Basis einer großen Bibliothek und einer aktiven Community moderne mathematische Definitionen schnell aufgebaut, doch propositions as types und abhängige Typen sind nicht der einzige Weg für Proof Assistants
  • Isabelle betont starke Automatisierung, hohe Lesbarkeit und die Vermeidung abhängiger Typen als Vorteile und setzt die LCF-Tradition fort, in der die Beweisprüfung auch ohne proof objects über die Abstraktionsbarriere des Kernels organisiert wird
  • Mit dem zusätzlichen Trend, dass KI strukturierte Beweise aufbereitet und in andere Systeme übersetzt, könnte der Druck weiter sinken, nur ein einziges Werkzeug als absoluten Maßstab zu sehen

Frühe Systeme und andere Traditionslinien

  • AUTOMATH

    • AUTOMATH enthielt bereits 1968 die meisten Elemente, die für die Formalisierung von Mathematik nötig sind
    • 1977 formalisierte Jutting mit AUTOMATH Landaus Foundations of Analysis und behandelte ausgehend von reiner Logik sogar die Konstruktion der komplexen Zahlen
    • Er verwendete Äquivalenzklassen und Mengen rationaler Zahlen und bewies auch die Dedekind-Vollständigkeit der reellen Zahlengeraden formal
    • Dieses Ergebnis wurde 20 Jahre lang nicht wieder erreicht; erst Mitte der 1990er Jahre entstanden erneut Formalisierungen der reellen Zahlen in John Harrisons HOL Light und Jacques Fleuriots Isabelle/HOL
    • Die Notation war sehr unhandlich, und es gab überhaupt keine Automatisierung, sodass die Beweise lang und schwer lesbar waren
    • Dennoch sei das System beim Umgang mit Äquivalenzklassen besser als Rocq; anders als die setoid hell, mit der Rocq-Nutzer kämpfen, führte Jutting die Formalisierung von Äquivalenzklassen ruhig und konsequent durch

  • Boyer und Moore

Die Entwicklung nach LCF

  • Edinburgh LCF konzentrierte sich auf Programmiersprachentheorie, doch die Idee, in Proof Assistants eine funktionale Sprache als Metasprache zu verwenden, verbreitete sich weithin
  • Mehrere Gruppen in Cambridge, INRIA, Cornell und anderswo nutzten ML, um Werkzeuge wie frühe HOL-Systeme, Coq (heute Rocq) und Nuprl zu entwickeln
  • Die HOL-Gruppe konzentrierte sich auf Hardware-Verifikation, benötigte wegen der Verifikation von Gleitkomma-Hardware aber auch reelle Analysis
  • John Harrison bewies in der HOL-Familie über die Cauchysche Integralformel ernsthafte mathematische Resultate wie den Primzahlsatz
  • Unter dem Ziel, möglichst viele der 100 theorems zu verifizieren, lag HOL Light häufig in der Spitzengruppe
  • Bis 2014 hatten Systeme dieser Linie mehrere fortgeschrittene Sätze formalisiert
  • Diese Sätze hatten meist lange und komplexe Beweise, und auch die Formalisierungsarbeit war von sehr großem Umfang; sie spielte eine Schlüsselrolle dabei, verbleibende Zweifel an den Sätzen zu verringern

Der Aufstieg der Lean-Community

  • Mathematiker sahen, dass frühere Formalisierungserfolge nicht bis zu den ausgefeilten Konstruktionen der modernen Mainstream-Mathematik wie Grothendieck schemes oder perfectoid spaces reichten
  • Tom Hales entschied sich dafür, solche Definitionen als Bibliothek aufzubauen, wählte Lean und legte den Schwerpunkt eher auf die Akkumulation von Definitionen als auf einzelne Beweise
  • Er stellte diese Richtung im Programm Big Proof vor, wo auch ähnliche Ideen diskutiert wurden
  • Kevin Buzzard hörte dies und beschloss, Lean in der Lehre auszuprobieren, woraufhin sich die Verbreitung beschleunigte
  • Als wichtiger Wendepunkt der Lean-Community wird genannt, dass sie sich von der lange dominierenden Fixierung auf konstruktive Beweise in Rocq löste
  • Intuitionismus entstand nach Russells Paradoxon und hatte auch bestimmte Implikationen für den Begriff der reellen Zahl
  • Die Martin-Löf-Typentheorie ist eindeutig eine intuitionistische Form des Formalismus, doch bei Rocq sei die Lage nicht so einfach
  • Dennoch tauchten in Rocq-bezogenen Arbeiten konstruktive Beweise immer wieder auf, auch dort, wo sie irrelevant oder bedeutungslos waren; diese Tendenz habe die mathematische Anwendung von Rocq behindert und Lean Raum gegeben

propositions as types und der Unterschied zu LCF

  • Propositions as types ist die Dualität zwischen den logischen Symbolen ∀, ∃, →, ∧, ∨ und den Typkonstruktoren Π, Σ, →, ×, +
  • Dieses Schema ist elegant und theoretisch produktiv, aber nicht der einzige Weg
  • Wenn man einen Proof Assistant auf Software verengt, die Beweise nach dem Prinzip propositions as types prüft, fällt der größte Teil der Forschung des letzten halben Jahrhunderts aus der Definition heraus
  • Dann blieben nur Rocq, Lean und Agda übrig
  • Selbst AUTOMATH ist kein Beispiel für propositions as types; es gibt zwar Elemente ähnlich zu Π und →, doch die Logik wird wie in gewöhnlichen Logiklehrbüchern durch Axiome festgelegt
  • De Bruijn sah schon vor 50 Jahren die Notwendigkeit einer Trennung von Typen und Aussagen
  • Ein typisches Beispiel ist die Division, die drei Argumente erhalten muss; da der Wert von (x/y) von einem Beweis für (y \ne 0) abhängt, ist proof irrelevance erforderlich
  • Auch die Vorstellung, der LCF-Ansatz sei dasselbe wie propositions as types, sei sachlich falsch
  • In Rocq und Lean gibt es mit Prop einen Sort für Aussagen; dort werden alle Beweisobjekte derselben Aussage als derselbe Wert behandelt, was proof irrelevance liefert
  • Das bedeutet jedoch nicht, dass riesige Beweisobjekte verschwinden; im realen System sind sie weiterhin vorhanden
  • Robin Milners zentrale Einsicht war, dass in LCF Beweisobjekte selbst gar nicht nötig sind
  • Wenn man den Beweiskernel in einen abstrakten Datentyp von ML legt und die Inferenzregeln als Konstruktoren bereitstellt, kann man Beweise dynamisch prüfen
  • Dank der abstraction barrier von ML sei Betrug unmöglich
  • Dass riesige Terme, die nichts weiter anzeigen, dennoch Dutzende MB belegen, wirkt gerade im Zeitalter von RAMmageddon besonders unvernünftig
  • Kritisiert wird auch, dass es sogar Forschung dazu gibt, solche unnötigen Terme eleganter zu machen

Gründe, Isabelle zu wählen

  • Wenn Kollegen Lean verwenden, die Expertise des Teams bei Lean liegt und die benötigten Grundlagenbibliotheken in Lean vorhanden sind, ist es natürlich, Lean zu verwenden
  • Wenn man jedoch frei wählen kann, gibt es klare Gründe, Isabelle in Betracht zu ziehen

  • Automatisierung

    • Als Vorteil wird die stärkste Automatisierung genannt; selbst im Vergleich zu den üblichen „hammer“-Werkzeugen gebe es nichts, das mit sledgehammer mithalten könne
    • Auch Computeralgebra müsse gesondert betrachtet werden

  • Lesbarkeit

    • In Bezug auf Lesbarkeit sei dies die beste Wahl, mit Isar-Beispielen als Beleg

  • Vermeidung abhängiger Typen

    • Weil es keine abhängigen Typen gibt, vermeidet man Universe-Levels und viele Merkwürdigkeiten, die Einsteiger verwirren
    • Auch in Leans mathlib sowie in Rocqs SSReflect und Mathematical Components werde der Einsatz abhängiger Typen nicht empfohlen
    • Die zentrale Schwierigkeit abhängiger Typen besteht darin, dass bei korrekter Implementierung Typprüfung selbst unentscheidbar wird
    • Das liege daran, dass die Entscheidung über Gleichheit unentscheidbar ist; anfangs sei dies als selbstverständlich akzeptiert worden
    • Etwa ab 1990 verlagerte sich der Konsens dahin, Typprüfung entscheidbar zu machen, indem man Gleichheit auf definitional/intensional equality abschwächt
    • In der Folge sind (T(N+1)) und (T(1+N)) verschiedene Typen
    • Diese Einschränkung wirkt sich auch auf reale Beweise aus, und die Prüfung von definitional equality bleibt weiterhin rechenintensiv

Moderne Mathematik auch ohne abhängige Typen

Zukünftige Richtung und KI

  • Lean macht vieles richtig und unterstützt sogar verschachtelte Beweisblöcke, sodass es potenziell eine ausreichend gut lesbare Beweissprache werden kann
  • Nun müsse die Lean-Community solche Funktionen auch tatsächlich nutzen; Isabelle-Nutzer täten dies größtenteils bereits
  • Wichtiger als maschinenprüfbare Beweisobjekte ist die Transparenz des Beweistexts, den Menschen wirklich lesen können
  • Der Aufstieg der KI macht diesen Unterschied noch deutlicher
  • Von KI erzeugte Beweise sind oft chaotisch, lassen sich aber mit sledgehammer leicht aufräumen; wenn die Struktur gut ist, bleiben sie auch bei übermäßigen Details lesbar
  • So lässt sich der Ablauf leichter nachvollziehen und auf eine einfachere Form reduzieren
  • Kürzlich erschien auch Forschung, in der Sprachmodelle direkt sledgehammer aufrufen
  • KI kann auch gut lesbare strukturierte Beweise direkt von einem Proof Assistant in einen anderen übersetzen
  • Dadurch sinkt auch die Belastung, sich überhaupt für ein bestimmtes System entscheiden zu müssen

Ergänzung zum ausgelassenen Mizar

  • Die Geschichte der mathematischen Formalisierung ist ohne Mizar und seine umfangreiche Mathematikbibliothek nicht vollständig
  • Auch Isabelles Isar-Sprache wurde stark von Mizar beeinflusst
  • Das Auslassen von Mizar wird eigens korrigiert, und im nächsten Beitrag soll Mizar behandelt werden

Verwandte Beiträge

1 Kommentare

 
GN⁺ 1 일 전
Hacker-News-Kommentare

  • Die meisten HN-Leser sind eher Programmierer als Mathematiker, deshalb ist es wohl praktischer, Lean eher aus Programmierperspektive als über mathematische Beweise zu betrachten.
    Als Buch, das Lean aus Sicht der funktionalen Programmierung behandelt, ist https://leanprover.github.io/functional_programming_in_lean/ ziemlich gut.
    Ich lerne Lean auch gerade erst, daher habe ich vielleicht einen etwas rosaroten Blick als Anfänger, aber mein Ziel ist eher so etwas wie das aktuelle lean-zip-Beispiel: Code ganz normaler Programmierer wie echte Kompressions-/Dekompressionsalgorithmen zu schreiben und zu beweisen.
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • Beim Lesen dieses Buchs habe ich mit Lean selbst einen einfachen Computeralgebra-Simplifizierer ausprobiert.
      https://github.com/dharmatech/symbolism.lean
      Das ist ein Port von C#-Code, und Leans Ausdrucksstärke ist erstaunlich groß.
    • Für so einen Zweck wäre Dafny vielleicht auch eine ähnliche Option.
      Ich erinnere mich, dass es vor einiger Zeit etwas Aufmerksamkeit bekam, aber ich habe das Feld zuletzt nicht genauer verfolgt.
    • Ich erinnere mich an Experimente aus den 1990er-Jahren mit Korrektheitsbeweisen für Software, bei denen am Ende in den Beweisannotationen mehr Fehler steckten als in der eigentlichen Software.
      Und ich sehe noch zwei weitere Hürden. Erstens ist es schon schwer genug zu wissen, was Software eigentlich tun soll, und was Nutzer tun wollen, ist nicht unbedingt dasselbe, wofür Kunden bezahlen.
      Zweitens ist die Arbeitsqualität vieler Entwickler so niedrig, dass man schwer erwarten kann, dass sie eine Wahrheitssprache besser beherrschen als etwa Java.
      Das Zweite könnte allerdings verschwinden, wenn solche Aufgaben durch AI-Systeme ersetzt werden, die die nötige Sorgfalt aufbringen; dann könnte sich die Lage ändern.
    • Ich frage mich, wie es mit nichtfunktionaler Programmierung aussieht.
      Auch funktionale Programmierung ist für die meisten Programmierer vermutlich ungefähr so wenig relevant wie die Mathematik, die sie bereits links liegen gelassen haben.

  • Der Autor scheint Lean ziemlich missverstanden zu haben, was umso überraschender ist, weil er in diesem Gebiet eigentlich kompetent wirkt.
    Er scheint zu glauben, Lean bewahre Beweisobjekte vollständig auf und prüfe am Ende ein einziges riesiges Beweisobjekt, in dem alle Definitionen expandiert wurden, aber das ist ziemlich weit von der Realität entfernt.
    Lean implementiert die Optimierung, die der Autor als Vorteil von LCF hervorhebt, im Wesentlichen genauso. Als Bild kann man sagen: Der Beweis wird geführt, während man die Tafel zwischendurch wieder abwischt.
    Wenn man in Lean4 etwas als theorem und nicht als def schreibt, wird dieses Beweisobjekt danach nicht mehr verwendet; das ist nicht bloß eine Optimierung, sondern eine Kerneigenschaft der Sprache. theorem ist opaque.
    Selbst wenn der Beweisterm noch existiert, dann nur, damit der Benutzer ihn im interaktiven Modus sehen kann; dem Kernel ist es nicht einmal möglich, sich dafür zu interessieren, was dieses Beweisobjekt war.

    • Das ist eher ein konzeptioneller Unterschied als einer der Implementierung.
      In LCF sind Beweise und Terme verschieden, und ich finde, das sollte eigentlich auch so sein. Diese Art von Curry-Howard-Verwechslung ist unnötig, aber viele halten sie für den einzigen Weg, Mathematik am Computer zu machen.
      Wenn man will, kann man auch in LCF Beweise speichern und nutzen, und in Lean kann man sie, wenn man will, per Optimierung wieder entfernen.
    • In der Theorie abhängiger Typen ist ein Beweisobjekt einfach ein Term, der einen bestimmten Typ bewohnt. Bedeutet das dann, dass die Lean-Implementierung Beweise konstruieren kann, ohne solche Terme überhaupt zu erzeugen?
    • Klingt richtig.
      Der abstrakte Typ-Ansatz spart vielleicht etwas Speicher, aber nur um einen konstanten Faktor und nicht asymptotisch.
      Beschwerden darüber, dass Lean zig MB verschwende, wären in den 1980er- oder 1990er-Jahren relevant gewesen, heute ist das womöglich kein so entscheidender Vorteil mehr.

  • Man hört oft, Lean sei gut für funktionale Programmierung, aber wenn man von Agda kommt, fühlt es sich eher wie ein etwas grober Rückschritt an.
    Auch tactic soll gut sein, aber nach meiner Erfahrung sind Coqs tactics mächtiger und angenehmer zu benutzen.
    Das mag alles ein Bias des ersten Eindrucks sein, aber bisher scheint Leans Stärke weniger darin zu liegen, eine Sache am allerbesten zu können, sondern eher darin, insgesamt solide zu sein und eine große Community zu haben.
    Ich verstehe, warum das attraktiv ist, aber es ist auch etwas schade, weil dabei ein wenig Schönheit und Kraft verloren zu gehen scheinen.

    • Am Ende ist das auch ein Argument über Netzwerkeffekte.
      Solche Effekte wirken im Moment selbst oft dauerhaft, halten in Wirklichkeit aber nicht so lange, wie man denkt. Wenn nur das zählte, müsste Perl heute noch ein Riese sein.
      Bei Lean war vor allem der frühe Aufbau einer großen Bibliothek wichtig, ähnlich wie CPAN einst für Perl.
      Aber wenn man Skalierungsgesetze betrachtet, steigt der Wert einer großen Bibliothek für die meisten Nutzer wahrscheinlich nur ungefähr logarithmisch mit ihrer Größe.
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Anfangs wirkt dieser Vorsprung unüberwindbar, aber ab einem gewissen Punkt wird Benutzerfreundlichkeit wichtiger, ohne dass man die reine Größenordnung aufholen müsste.
      Außerdem ist das Portieren mathematischer Bibliotheken eine Aufgabe, die gut zu LLMs passt. Die Quelle ist verifiziert, das Ziel ist verifizierbar, und der Weg der Herleitung lässt sich meist übertragen.
      Anders gesagt senken LLMs vermutlich auch die Hürde, auf kleineren Plattformen zu arbeiten. Wenn ich ihre Bibliothek auf meine Plattform portieren kann, kann ich vermutlich auch meine Beweise dorthin portieren.
    • Eher bedeutet das doch, dass die Community endlich gereift ist und angefangen hat, echte Arbeit zu erledigen.
      Das perfekte Tool ist nicht der entscheidende Punkt; wichtiger ist, mit einem hinreichend guten Tool tatsächlich etwas zu schaffen.
    • Agda ist vielleicht besser als Proof Checker, aber keine praktische Wahl, um Software zu bauen.
      Lean könnte tatsächlich noch zu einem Nachfolger von Haskell werden; es scheint das Potenzial zu haben, zu einer funktionalen Sprache für Softwareentwicklung heranzuwachsen.
    • Ich habe Agda ein wenig und Lean etwas mehr benutzt, und allgemeine funktionale Programme zu schreiben war in Lean viel einfacher als mathematische Beweise.
      Der Unterschied lag für mich vor allem bei der Tool-Unterstützung. Die Agda-Dokumentation ist schwach, Installation und Betrieb im eigenen System sind umständlich, und faktisch wird man stark in Richtung Emacs gedrängt.
      Lean hat dagegen in der eigenen Dokumentation sogar Anleitungen zum Schreiben eines cat-Utilities und bietet insgesamt eine deutlich modernere Tooling-Erfahrung.
    • Mich würde interessieren, was genau an funktionaler Programmierung in Agda so gut ist.
      Das Lob betrifft meist dependent pattern matching, und da wirkt Lean auf mich ziemlich schwach.
      Wenn sich Agda aber auch bei allgemeinem FP freundlicher anfühlt, würde ich gern hören, woran das konkret liegt.

  • Isabelle/HOL hat als Sprache durchaus Qualitäten, aber beim Tooling tiefe Mängel, die über den Desktop-zentrierten Ansatz noch hinausgehen.
    Die Sprache ist nicht grundsätzlich besser als Lean, nur anders, und ich stimme auch einigen Kritikpunkten an abhängigen Typen zu.
    Letztlich haben die beiden Sprachen unterschiedliche Trade-offs gemacht, und diese Entscheidungen haben sie jeweils in ihren Bereichen zu ziemlich effizienten Werkzeugen gemacht. Der Bereich formaler Beweise ist so breit, dass jedes Paradigma andere Stärken und Schwächen hat, und Lean ist eben auf einen anderen Ausschnitt spezialisiert.
    Sledgehammer ist gut, aber dass es in Lean etwas Ähnliches geben wird, scheint nur eine Frage der Zeit zu sein.
    In der Erkundungsphase kann das nützlich sein, aber es ist ressourcenhungrig, und auch wenn es Beweise verkürzt, sehe ich in veröffentlichtem Code lieber die vollständigen Schritte des Beweises direkt, statt eines halbmagischen by sledgehammer.
    Dagegen ist die Entwicklung von Isabelle selbst viel schmerzhafter als bei Lean, vor allem die Kommunikation mit den Entwicklern.
    Diese Haltung auf der Mailingliste nach dem Motto Es gibt keine Bugs, nur unerwartetes Verhalten wirkte kindisch und unprofessionell.
    Und sich über den RAM-Verbrauch von Systemen ähnlich Lean lustig zu machen, ist angesichts von Isabelles eigenem Speicherfraß ziemlich komisch.

    • Das Problem hier ist, dass es überhaupt nicht trivial ist, UNSAT-Zertifikate in eine Form zu bringen, die sich schnell prüfen lässt.
      Das ist im Grunde fast so schwierig wie der Einsatz formaler Beweise selbst.
    • Als ich zuletzt nachgesehen habe, nutzte Isabelle/HOL meines Wissens einen angepassten Emacs-Modus als Interface.
      Vielleicht verwechsle ich es aber auch mit einem anderen HOL.
    • Ich weiß nicht, was Sledgehammer ist, aber der Beschreibung nach klingt es fast wie Mathlibs grind.
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Das Interessante an Lean ist, dass Lean eine Sprache ist, während die Leute in Wirklichkeit meist über Mathlib sprechen, also eine Bibliothek.
    Die Mathlib-Macher wirken ziemlich pragmatisch, deshalb stecken sie klassische Logik in Leans Typen und verwenden intuitionistische Logik nur teilweise.

    • Das Beispiel zur Aussage vom ausgeschlossenen Dritten war falsch.
      „Etwas kann nicht zugleich wahr und falsch sein“ ist nicht der ausgeschlossene Dritte, sondern der Satz vom Widerspruch.
      Der ausgeschlossene Dritte bedeutet, dass entweder p wahr ist oder not p.
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • Die Informatikseite baut inzwischen ihre eigene CSLib.
      https://www.cslib.io https://www.github.com/leanprover/cslib
      Intuitionistische Logik hat ihren eigentlichen Sinn darin, mathematische Argumente in berechenbare Konstruktionen zu überführen, daher ist es interessant, wie man dieses Problem dort behandeln wird.
      Tatsächlich unterliegt man ohnehin schon irgendeiner Form konstruktiver Einschränkung, sobald man in Lean Algorithmen schreibt, und für diesen Zweck könnte diese Logik bereits ausreichen.
    • Mich erinnert das an den Witz über die fünf Phasen, konstruktive Mathematik zu akzeptieren.
      Verleugnung, Wut, Verhandeln, Depression, Akzeptanz.
      Auch ein einschlägiger Vortrag und Text von Andrej Bauer sind sehenswert.
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Hier müsste es nicht intuitive logic, sondern intuitionistic logic heißen.
    • Trotz all dieser Einschränkungen und Sackgassen frage ich mich, wann und warum man intuitionistische Logik bevorzugen würde.

  • Ich finde, wir brauchen mehr solche Texte.
    Gegen das Gruppendenken, bei dem alle wie selbstverständlich benutze einfach X sagen, gibt es zumindest immer gute Gründe, sich Alternativen einmal ernsthaft anzusehen.
    Selbst wenn man am Ende die Alternative verwirft und sich für den Mainstream entscheidet, ist es besser, die Landschaft zu kennen und bewusst zu wählen.

    • Dem stimme ich nicht vollständig zu.
      Schon jetzt bauen wir viel zu viele Frameworks und Alternativen, vermutlich oft einfach, weil es Spaß macht.
      Statt bestehende Werkzeuge zu verbessern oder einfach reale Arbeit voranzubringen, vermehrt man endlos Sprachen, Bibliotheken und Build-Tools.
      Ich glaube, es wäre besser, wenn wir nur halb so viele Sprachen, Bibliotheken und Build-Tools hätten wie heute.
    • Es kommt letztlich auf den Kontext an.
      Je weiter man sich vom Mainstream entfernt, desto schlechter wird die Dokumentation, desto mehr Bugs tauchen in wenig erkundeten Ecken auf, und desto weniger Leute können helfen.
      Sobald man mehr als zwanzig Optionen hat, ist es im Durchschnitt vernünftig, einfach die Standardwahl zu treffen und weiterzumachen. Aufmerksamkeit ist begrenzt; wenn man zu jeder Abhängigkeit erst einen Untersuchungsbericht schreibt, löst man am Ende das eigentliche Problem nicht.
      Zwei Ausnahmen gibt es: wenn das Standardwerkzeug wirklich nicht zu meinem Use Case passt oder wenn das Standardwerkzeug selbst stark mit dem Kernproblem überlappt, das ich eigentlich lösen will.

  • Diese Diskussion erinnert mich an Texte, die auf die Grenzen von Python im wissenschaftlichen Rechnen hinweisen.
    Sobald sich um ein halbwegs gutes Werkzeug herum eine Community mit kritischer Masse bildet, überlagert das die meisten anderen Faktoren.
    Es entsteht Momentum, Tutorials, Erklärtexte und bessere Dokumentation sammeln sich an, und irgendwann erreicht das Ganze praktisch Fluchtgeschwindigkeit.
    Lean scheint gerade genau an diesem Punkt zu sein, zumal es mit Terrance Tao sogar einen sehr prominenten Fürsprecher hat.
    Deshalb ist „Sprache X ist besser“ nicht unbedingt falsch, verfehlt aber leicht die eigentlich wichtige Frage.
    Entscheidend ist, ob sie wirklich besser ist als das Werkzeug, das alle kennen, sofort einsetzen können und in das viel mehr Zeit zur Verbesserung investiert wird.
    Am Ende wirkt das wie worse is better, oder wie eine Situation, in der gut und populär bereits gut genug ist.

    • Ich finde den Punkt gut, dass LLMs die Übersetzung zwischen verschiedenen formalen Systemen ziemlich effektiv machen könnten.
      Gerade in diesem Bereich lässt sich das Übersetzungsergebnis zu großen Teilen automatisch verifizieren, sodass die Wahl selbst vielleicht gar nicht so entscheidend ist.
    • Aber im AI-Zeitalter ist kritische Masse viel weniger wichtig.
      AI kann auch ohne riesige Community-Bibliotheken selbst Code schreiben und liest Dokumentation und Spezifikationen direkt, selbst wenn nicht Millionen Tutorials im Netz herumschwirren.
      Man muss Sprachen ohne Arbeitsmarkt nicht mehr meiden. AI baut keine Karriere auf, sondern erledigt einfach die Aufgabe, die gerade ansteht.
      Dadurch steigen die Chancen für kleine Sprachen und DSLs, die früher kaum eine Chance gehabt hätten.
      Die lange anhaltende sprachliche Monokultur in der Programmierung könnte durch AI enden.

  • Die Aussage „Fast alles, was heute in irgendeinem System formalisiert ist, hätte auch in AUTOMATH formalisiert werden können“ ist ungefähr so, als würde man sagen, was heute in modernen Sprachen geschrieben wird, hätte man vor 50 Jahren auch in Assembler schreiben können.
    Technisch stimmt das, ökonomisch ist es aber eine völlig andere Sache.

    • Assemblersprachen sind meist turing-vollständig, aber ich weiß nicht genau, was auf der Seite von Beweisengines die wirklich passende Entsprechung dazu wäre.

  • Vor etwa 15 Jahren habe ich versucht, mich in Coq/Rocq und einige andere Werkzeuge einzuarbeiten, aber weniger die Konzepte als vielmehr die Software selbst war kaum zu durchschauen.
    Das Merkwürdige an Proof Assistants bzw. interaktiven Theorembeweisern ist, dass sie durch ihren interaktiven Charakter eine Kopplung aus Sprache und IDE bilden und in der Praxis auch stark miteinander verflochten sind.
    Deshalb ist es schwer, nur über die Sprache isoliert zu sprechen; man muss immer auch die Umgebung mit betrachten, in der sie verwendet wird.
    Ich bin selbst kein glühender Fan von VS Code, aber dass eine von sehr vielen Menschen genutzte, mit viel Geld gepflegte erweiterbare IDE den Umgebungen der Alternativen weit voraus ist, steht außer Frage.
    Auch hervorragende Einstiegspfade wie das Natural Numbers Game scheinen überhaupt erst dank der Hackbarkeit und des Ökosystems von VS Code möglich zu sein.
    Was mir beim Lernen von Lean allerdings Sorgen macht, ist, dass Syntax-Erweiterbarkeit ein zweischneidiges Schwert ist.
    Wenn man die Sprache einmal gelernt hat, möchte man Code in dieser Sprache lesen können; wenn aber jedes Projekt anfängt, massenhaft eigene DSLs zu bauen, kann das leicht außer Kontrolle geraten.
    Am Ende hängt das davon ab, wie viel Selbstdisziplin Community und Ökosystem aufbringen, und deshalb beobachte ich das mit einer Mischung aus Hoffnung und Sorge.

  • Lean ist weder der von Mathematikern am meisten geliebte Proof Assistant noch das am besten geeignete Werkzeug für formale Softwareverifikation.
    Es kann aber beides ganz ordentlich und hat dafür das am schwersten zu gewinnende Gut erlangt: Momentum.
    Und im AI-Zeitalter wird dieses Momentum noch stärker, weil die Menge an offen verfügbarem, von Menschen geschriebenem Code direkt beeinflusst, wie gut Agenten neuen Code erzeugen können.