Mathematisches Schließen & formales Beweisen

Mathematik und Softwareverifikation leiden unter einem Vertrauensengpass: Beweise sind lang, die Zeit der Gutachter ist knapp und Fehler rutschen durch. Reasoning-LLMs können heute Lösungen entwerfen, und gekoppelt mit einem Beweisassistenten wie Lean 4 wird jeder Schritt von einem kleinen vertrauenswürdigen Kern geprüft, sodass ein erfundener Beweis automatisch abgelehnt wird. Das Ergebnis ist ein überprüfbarer KI-Anwendungsfall: Forschende erhalten Lemma-Suche und Beweisautomatisierung, Ingenieure verifizierten Code und Spezifikationen, Lehrende geprüfte Lösungen.

Problem & Nutzen

• Heute: Einen Satz in einem Beweisassistenten zu formalisieren ist langsame Expertenarbeit; Mathematiker prüfen Fachartikel von Hand; die formale Verifikation von Software, Protokollen oder Smart Contracts beschränkt sich auf wenige Spezialistenteams.
• KI-Nutzen: (1) Lösen, wobei Reasoning-Modelle Wettbewerbs- und Forschungsprobleme in natürlicher Sprache bearbeiten; (2) formales Beweisen, wobei Modelle Lean-/Isabelle-Beweise erzeugen, die der Kern akzeptiert oder ablehnt; (3) Autoformalisierung, die informelle Aussagen und Fachartikel in formale übersetzt; (4) Beweispflege, die durch Bibliotheksaktualisierungen gebrochene Beweise repariert.
• Zentrale Eigenschaft: Der Prüfer ist exakt, daher kann man der Ausgabe vertrauen, ohne dem Modell zu vertrauen. Damit ist dies eines der wenigen KI-Gebiete mit einem perfekten Belohnungssignal für bestärkendes Lernen.
• Belege für den Fortschritt: DeepMinds AlphaProof und AlphaGeometry 2 erreichten bei der IMO 2024 Silbermedaillen-Niveau, und 2025 meldeten mehrere Systeme (Google Gemini Deep Think, OpenAI und das Start-up Harmonic für formale Beweise mit Aristotle) Leistungen auf Goldmedaillen-Niveau bei der IMO [1][2]. Benchmarks wie miniF2F sind nahezu gesättigt, während Testsammlungen auf Forschungs- und Bachelor-Niveau wie PutnamBench weit von einer Lösung entfernt sind [3][4].
• Verlässliche, belegte Produktivitätszahlen für die Industrie gibt es noch nicht; messen Sie vor Ort.

Varianten

• Forschungsmathematik: Lemma-Suche, Vorschläge für Beweisschritte, Formalisierung von Fachartikeln in Mathlib.
• Bildung: schrittweise geprüftes Tutoring und Überprüfung von Übungsaufgaben (siehe EDU-001); Prüfung von Beweisen von Studierenden.
• Software- und Protokollverifikation: Beweise über Code, Kryptografie, Smart Contracts und verteilte Systeme (Dafny, Verus, Lean, Isabelle, Rocq); Verbindungen zu CODE-019 und SCI-016 (Hardwareverifikation).
• Quantitative Modellierung: Solver-gestütztes Schließen für Finanz-, Versicherungsmathematik- oder Ingenieurformeln mit Computeralgebra (SymPy, Mathematica, SageMath) und SMT-Solvern (Z3, cvc5).
• Private Nutzung: Hausaufgabenhilfe und Rätsellösen mit einem Reasoning-Chatmodell; die formale Prüfung ist optional.

So funktioniert es

1. Problem (natürliche Sprache / formale Aussage)
2. Autoformalisierung (LLM: Aussage
3. Lean 4) [Mensch prüft die Aussage]
4. Prämissen-Retrieval (Embedding-Suche über Mathlib / Projektbibliothek)
5. Beweissuche (LLM schlägt Taktiken oder ganze Beweise vor; Best-First- oder Baumsuche; Sampling in großem Maßstab)
6. Verifikation (Lean-Kernel / Isabelle / Rocq kompiliert; Fehler werden an das Modell zurückgegeben)
7. Reparaturschleife (Agent liest Fehlermeldungen, ändert, versucht erneut; zerlegt in Lemmata)
8. akzeptierter Beweis + Audit (Prüfung der Aussagetreue durch einen Menschen)

• Reasoning-Modelle erzeugen informelle Strategien; spezialisierte Beweiser erzeugen Lean-Code für Taktiken oder ganze Beweise, trainiert mit bestärkendem Lernen gegen den Prüfer auf großen synthetischen Problemmengen.
• Werkzeugnutzung: Agenten rufen das Lean REPL oder den Language Server auf, die Automatisierung exact?/aesop/omega, Sledgehammer (Isabelle), CAS- und SMT-Solver.
• Mensch-in-der-Schleife (Human-in-the-Loop): Dem Beweis kann man vertrauen, aber die formale Aussage gibt die gemeinte Behauptung womöglich nicht wieder. Ein Fachexperte muss Aussage, Definitionen und Axiome prüfen (auf sorry, hinzugefügte Axiome und leere Wahrheit achten).

Datenaufbereitung

Der Datenbedarf ist im Vergleich zu anderen Anwendungsfällen gering: Problemstellungen, informelle Beweise, formale Bibliotheken (Lean Mathlib, Isabelle AFP) und für die Verifikation Spezifikationen und Quellcode. Diese liegen in Fachartikeln (LaTeX, PDF), Kursunterlagen, Wikis, Git-Repositories und in den Köpfen der Ingenieure. Typische Lücken: informelle Spezifikationen, mehrdeutige Notation, fehlende formale Aussagen zu informellen Ergebnissen, verstreutes Vorlesungsmaterial und kein Benchmark mit eigenen Problemen.

Schritte der Aufbereitung: Probleme mit vereinbarten formalen Aussagen sammeln; zentrale Definitionen in die Bibliothek des Beweisassistenten übertragen (Autoformalisierung mit menschlicher Prüfung); Code und Spezifikationen in der Versionsverwaltung strukturieren (PREP-009); Terminologie und Konventionen festhalten (PREP-015); gelöste Beispiele als Referenz sammeln (PREP-016); und eine kleine Evaluierungsmenge eigener Probleme aufbauen (PREP-018). Werkzeuge: Lean mit Mathlib, Extraktion im Stil von LeanDojo, Pandoc für die LaTeX-Konvertierung.

Rechnen Sie nur mit etwa 10 bis 20 Prozent des Aufwands für die Datenaufbereitung; der meiste Aufwand fließt in die korrekte Formalisierung der Aussagen. Siehe GUIDE-003.

Umsetzungswege

Welcher Weg für wen

• Entwickler: Weg B. Reasoning-Modell-APIs in Kombination mit einer lokalen Lean- oder Isabelle-Toolchain liefern mit wenig Einrichtung die stärksten Ergebnisse.
• Unternehmen (Verifikation, sicherheitskritische Software): Weg B. APIs plus hauseigene Beweiswerkzeuge eignen sich für Pilotprojekte; halten Sie proprietäre Spezifikationen aus Prompts heraus oder nutzen Sie EU-Regionen.
• Öffentlicher Sektor (Hochschulen, Schulen): Weg C. Offene Beweiser und Open-Weight-Modelle auf Hochschul-Rechenleistung vermeiden Lizenzkosten und halten die Forschung reproduzierbar.
• Privat: Weg A. Chat-Assistenten für Endverbraucher mit einer kostenlosen Lean-Installation reichen zum Lernen und für Hobbyzwecke.

Weg A — Kaufen (Standardsoftware)

• Reasoning-Assistenten: Frontier-Chatprodukte mit erweitertem Denken (Anthropic Claude, OpenAI, Google Gemini Deep Think, Mistral, EU) für informelle Mathematik; Computeralgebrasysteme (Wolfram, Maple) mit KI-Oberflächen.
• Formale Werkzeuge: Harmonics Aristotle (Lean-Beweise als Dienst), Axiom Math und Math Inc (Produkte zur Autoformalisierung, früher Zugang). Verifikationswerkzeuge: Imandra (UK), Certora (Smart Contracts), AWS Zelkova/Cedar für die Verifikation von Richtlinien.
• Wählen Sie A, wenn: Sie gelegentlich Hilfe oder einen schnellen Piloten brauchen; formale Verifikation im großen Maßstab ist eine Spezialistenleistung.

Weg B — Auf Cloud-KI-Diensten aufbauen (empfohlen)

• Modelle: Frontier-Reasoning-Modelle über API (Claude, Gemini, GPT, Mistral in EU-Regionen), gesteuert von einer Agentenschleife, die eine Lean-4-+-Mathlib-Sandbox aufruft; Compilerfehler zurückführen; Versuche und Kosten begrenzen.
• Stack: Lean 4 und Mathlib, LeanDojo oder das Lean REPL für die programmatische Interaktion, Lean Copilot für Vorschläge im Editor, Suche über Mathlib-Docstrings mit einem Embedding-Modell [5][6].
• Integration: CI, die jeden Beweis mit sorry oder neuen Axiomen ablehnt; Ergebnisse als Zertifikate neben dem Code gespeichert.

Weg C — Selbst betreiben (Open Source)

• Beweiser mit offenen Gewichten: DeepSeek-Prover-V2 (7B und 671B), Kimina-Prover, Goedel-Prover-V2 (Princeton), Seed-Prover (ByteDance, teilweise offen) und Qwen-/DeepSeek-Reasoning-Modelle für die informelle Arbeit [3].
• Betrieb: vLLM oder SGLang; Lean-Worker in Containern (viele parallele Compiler sind CPU-gebunden).
• Hardware: HW2/HW3 für Beweiser mit 7–32B; HW4 für Modelle der 671B-Klasse; die Suche braucht viele Stichproben je Problem.
• Beweisassistenten: Lean 4 (Lean FRO), Isabelle (TU München/Cambridge), Rocq (Inria, Frankreich), alle Open Source.

Weg D — Eigenes Training

Lohnt sich für Organisationen mit einer privaten formalen Bibliothek (z. B. ein verifiziertes Betriebssystem, Protokoll oder eine numerische Bibliothek). Einen Beweiser mit 7B–32B per Expert Iteration oder RL feinabstimmen (Feintuning), wobei der Beweisassistent die Belohnung liefert. Erforderlich sind ein Korpus aus formalen Aussagen (Tausende), ein Rechenbudget für das Sampling und Verifikationsingenieure. Öffentliche Rezepte existieren [3].

Stand der Technik (2026)

• Wettbewerbsmathematik liegt bei den besten Systemen im Wesentlichen auf Goldmedaillen-Niveau, sowohl in natürlicher Sprache als auch in Lean [1][2]. Offene Modelle liegen hinter geschlossenen, der Abstand bei miniF2F ist aber klein; PutnamBench und Aufgaben auf Forschungsniveau bleiben schwierig, prüfen Sie daher vor der Modellwahl die aktuellen Ranglisten [3][4].
• Autoformalisierung ist das schwächste Glied: Aussagen sind oft unterschwellig falsch, daher konzentriert sich die Bewertung auf die Treue.
• Erzeugung ganzer Beweise plus agentische Reparatur hat in den meisten neueren Systemen die reine Baumsuche abgelöst.
• Formalisierungsprojekte (Mathlib, das von K. Buzzard geleitete Projekt zum Großen Fermatschen Satz) beginnen, KI für Routine-Lemmata zu nutzen; die KI-gestützte Formalisierung von Fachartikeln im großen Maßstab ist ein aktives Feld.
• Grenzen: Scheitern bei langen, neuartigen Argumenten; gültige, aber unleserliche Beweise; Abhängigkeit von der Abdeckung der Bibliothek; korrekter Beweis eines falsch formulierten Satzes; keine Garantie, dass ein Modell einen Beweis findet, selbst wenn es einen gibt.

Gemeinsame Bausteine & Kombinationen

• Gleicher Stack (llm-reasoning + llm-code + agent-framework): SCI-011 KI-Wissenschaftler-Agenten (erzeugte Behauptungen prüfen), CODE-019 und SCI-016 (formale Verifikation von Hardware/RTL), SCI-013 (Formalisierung von Anforderungen im MBSE).
• Hardware: Ein gemeinsamer vLLM-Server (HW3/HW4) bedient Reasoning, Programmieren und Beweisen; Lean-Worker brauchen nur CPU.
• Verwandt: AGENT-001 (allgemeine Agenten), EDU-001 (Tutoring mit Schrittprüfung).

Aufwand, Kosten & Kennzahlen

• Weg A: Tage; Abonnement oder Preis nach Nutzung.
• Weg B: 1–3 Monate für einen Agenten plus Lean-Sandbox; die Kosten werden durch viele Versuche je Problem bestimmt.
• Weg C: 3–6 Monate; GPU-Knoten plus Lean-Fachwissen.
• Weg D: 6+ Monate; erfordert Beweisingenieure.
• Kennzahlen: Erfolgsquote bei festem Budget (pass@k), Kosten je verifiziertem Beweis, Bestehensquote der Prüfung der Aussagentreue, Prüfminuten je Beweis durch Menschen, Anteil automatisierter Lemmata, Zeit für die Formalisierung eines Fachartikelabschnitts.

Menschen & Veränderung

Beziehen Sie die Geschäftsleitung für die Entscheidung über den Pilotumfang ein, die Abteilungsleitung oder die Professur als Prozessverantwortliche, Forschende, Ingenieure oder Lehrende als Anwender sowie die IT für Rechenleistung, API-Schlüssel und die Installation der Toolchain. Datenschutz ist selten ein Thema, da mathematische Inhalte nicht personenbezogen sind; fragen Sie die bzw. den Datenschutzbeauftragte(n) nur, wenn Arbeiten von Studierenden oder Beschäftigtendaten eingereicht werden (GUIDE-005). Spezifikationen von Unternehmen können Betriebsgeheimnisse sein: Legen Sie Regeln in der KI-Richtlinie fest (GUIDE-007).

Betriebsrat: in der Regel nein. Die Beweiswerkzeuge überwachen kein Verhalten, und der Beweisassistent prüft selbst Ergebnisse, nicht Personen. Protokolliert eine unternehmensweite KI-Plattform einzelne Prompts, kann § 87 Abs. 1 Nr. 6 BetrVG für die Plattform gelten, nicht für diesen Anwendungsfall. Informieren Sie den Betriebsrat trotzdem frühzeitig nach § 90 Abs. 1 Nr. 3; Schulen und Hochschulen beteiligen den Personalrat.

KI-Kompetenz: Art. 4 KI-Verordnung (AI Act) verlangt Maßnahmen, die die KI-Kompetenz der Beschäftigten fördern; zeigen Sie Kolleginnen und Kollegen, dass ein maschinell geprüfter Beweis verlässlich ist, die formale Aussage aber dennoch falsch sein kann (GUIDE-006). Starten Sie einen Piloten mit einer kleinen Gruppe an einigen echten Problemen. Typische Sorge: Täuschung in der Bildung oder Verlust mathematischer Fähigkeiten. Begegnen Sie ihr mit klaren Kursregeln, indem Menschen für das Formulieren und Deuten von Sätzen verantwortlich bleiben und der Prüfer als letzte Instanz gilt (GUIDE-008).

Risiken, Regulierung & Compliance

• KI-Verordnung (AI Act): minimales Risiko bei Forschungs- und Bildungsunterstützung (Art. 4 KI-Kompetenz gilt). Bildungseinsatz, der Lernende bewertet oder Zulassungen steuert, kann als Hochrisiko nach Anhang III gelten; reines Tutoring nicht. Die Verifikation von Sicherheitskomponenten (Medizinprodukte, Maschinen) bleibt den Branchenvorschriften unterworfen; die KI-Ausgabe ist ein Nachweis, keine Zertifizierung [7].
• DSGVO: normalerweise keine personenbezogenen Daten; werden Arbeiten von Studierenden oder Identitäten von Forschenden verarbeitet, gelten Hosting in der EU und ein Auftragsverarbeitungsvertrag (AVV).
• Geistiges Eigentum: unveröffentlichte Forschung und proprietäre Spezifikationen, die an eine Cloud-API gehen; bevorzugen Sie EU- Regionen oder Weg C bei sensiblen Inhalten.
• Risiken und Gegenmaßnahmen: falsch formalisierte Aussagen (Prüfung durch Experten), übermäßiges Vertrauen in informelle LLM-Beweise (Prüfung durch den Kern verlangen), versteckte Axiome/sorry (CI-Sperre), Benchmark-Kontamination in Herstellerangaben (an eigenen Problemen testen).

Erste Schritte

1. Installieren Sie Lean 4 und Mathlib; reproduzieren Sie einen kleinen Beweis von Hand, um die Verifikationsschleife kennenzulernen.
2. Lassen Sie ein Reasoning-Modell 20 Ihrer eigenen Probleme bearbeiten, zuerst informell, dann über eine Agentenschleife mit Lean REPL.
3. Probieren Sie einen offenen Beweiser (DeepSeek-Prover-V2 7B oder Goedel-Prover-V2) auf einer einzelnen GPU und vergleichen Sie mit einem API-Modell.
4. Ergänzen Sie CI-Prüfungen: kein sorry, keine neuen Axiome, festgelegte Mathlib-Version, Checkliste für die Prüfung der Aussagen.
5. Wählen Sie ein reales Ziel (eine Menge von Bibliothekslemmata oder eine Spezifikation) und verfolgen Sie einen Monat lang die oben genannten Kennzahlen.

Quellen

1. Google DeepMind — AI achieves silver-medal standard solving IMO problems (AlphaProof, AlphaGeometry 2) — https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
2. Google DeepMind — Advanced Gemini Deep Think achieves gold-medal standard at IMO 2025 — https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/
3. DeepSeek-Prover-V2 paper (arXiv 2504.21801) — https://arxiv.org/abs/2504.21801
4. PutnamBench — https://github.com/trishullab/PutnamBench
5. Lean programming language and theorem prover — https://lean-lang.org/
6. Mathlib4 — https://github.com/leanprover-community/mathlib4
7. Regulation (EU) 2024/1689 (AI Act) — https://eur-lex.europa.eu/eli/reg/2024/1689/oj
8. LeanDojo — https://leandojo.org/