Mathlib
Mathlib ist die größte gemeinsame Sammlung formalisierter Mathematik der Welt: Tausende mathematische Sätze und Beweise, die ein Computer Schritt für Schritt überprüfen kann. Sie bildet die Grundlage dafür, dass KI-Systeme mathematisches Denken erlernen und maschinell verifizieren können.
Mathlib ist eine riesige Bibliothek mathematischer Sätze und Beweise — aber nicht als PDF oder Lehrbuch, sondern in einer Form, die ein Computer lesen und vollständig überprüfen kann. Sie ist in einer Programmiersprache namens Lean geschrieben, die dafür entwickelt wurde, Mathematik maschinell zu formalisieren: also so präzise aufzuschreiben, dass kein Schritt unbewiesen bleibt. Mathlib enthält heute über 100 000 solcher formalisierter Lemmata und Sätze, von einfacher Arithmetik bis hin zu Gebieten, die typischerweise erst im Mathematikstudium auftauchen. Sie entsteht als offenes Gemeinschaftsprojekt und wächst kontinuierlich durch Beiträge von Mathematikerinnen, Mathematikern und Informatikern weltweit.
Mathlib als Trainingsgrundlage für KI
Für KI-Systeme, die mathematisch denken sollen, ist Mathlib aus einem einfachen Grund wertvoll: Jeder Beweis in der Bibliothek ist automatisch überprüfbar. Das ist bei normaler Mathematik nicht selbstverständlich. In Lehrbüchern stehen Beweise in natürlicher Sprache, und Fehler schleichen sich oft unbemerkt ein. In Mathlib hat hingegen jeder Schritt eine eindeutige Bedeutung — der Lean-Compiler akzeptiert ihn nur, wenn er logisch korrekt ist.
Das ist für KI-Training ein enormer Vorteil. Ein Modell, das auf Mathlib trainiert wird, bekommt nicht nur Beispiele gezeigt, wie Beweise aussehen. Es bekommt auch sofort Rückmeldung, ob sein eigener Versuch korrekt ist. So kann es durch gezieltes Ausprobieren lernen, ohne dass ein Mensch jeden Schritt kontrollieren muss. Genau dieses Prinzip — maschinell verifizierbares Feedback — macht Mathlib zu einem der wichtigsten Datensätze für KI-gestützte Mathematik.
Wie Beweise in Lean und Mathlib aufgebaut sind
Ein Beweis in Lean sieht auf den ersten Blick wie Code aus, folgt aber streng mathematischer Logik. Man beginnt mit einer Behauptung — zum Beispiel, dass die Summe zweier gerader Zahlen immer gerade ist. Dann liefert man eine Kette von Begründungen, jede einzeln formuliert. Der Compiler prüft jeden Zwischenschritt. Fehlt auch nur eine Begründung oder ist sie falsch, verweigert das System die Annahme.
Mathlib stellt dabei einen Werkzeugkasten zur Verfügung. Wer einen neuen Satz beweisen will, muss das Rad nicht neu erfinden. Er kann auf Tausende bereits bewiesene Aussagen zurückgreifen, die in Mathlib hinterlegt sind, und sie als Bausteine verwenden. Das ähnelt dem Zitieren bekannter Resultate in einem wissenschaftlichen Artikel — nur dass der Computer sicherstellt, dass alles lückenlos passt. Neue Beiträge werden von der Community geprüft und nach Annahme dauerhaft in die Bibliothek aufgenommen.
Mathlib in KI-Produkten und Forschungsprojekten
Mathlib taucht vor allem in der Forschung zu sogenannten Theorem-Provern auf — Systemen, die selbstständig mathematische Beweise finden sollen. Google DeepMind hat mit AlphaProof ein System vorgestellt, das auf formalisierter Mathematik in Lean trainiert wurde und 2024 mehrere Aufgaben der Internationalen Mathematikolympiade löste. Das wäre ohne eine Bibliothek wie Mathlib kaum möglich gewesen, denn das System brauchte eine strukturierte Wissensgrundlage, aus der es schöpfen konnte.
Auch andere Labore, darunter Teams bei Meta und verschiedenen Universitäten, nutzen Mathlib als Datenbasis für Experimente mit KI und formalem Beweisen. In Tech-News begegnet man dem Begriff meist im Zusammenhang mit Meldungen über KI-Fortschritte in der Mathematik. Ein typischer Irrtum dabei: Mathlib selbst ist keine KI. Es ist eine Wissensbasis — das Rohmaterial, aus dem KI-Systeme lernen können.
Darüber hinaus nutzen immer mehr Mathematikerinnen und Mathematiker Mathlib unabhängig von KI, einfach um ihre eigenen Beweise auf Korrektheit zu prüfen. Der Schritt vom handgeschriebenen Beweis zur formalisierten Version ist aufwendig, gilt aber als absolut zuverlässig. In einer Disziplin, in der ein einzelner Fehler jahrelange Arbeit entwerten kann, ist das ein starkes Argument.