Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

Technisches Resümee: Auf ein Brücken-Layer zwischen bibliographischem und formalisiertem mathematischem Wissen

Problemstellung
Das moderne mathematische Wissen ist derzeit über zwei strukturell unabhängige Infrastrukturen fragmentiert. Einerseits existieren bibliographische Datenbanken wie MathSciNet und zbMATH Open, die den menschenlesbaren Forschungsstand indizieren und Publikationsmetadaten, Zitiernetzwerke sowie Expertenrezensionen erfassen. Andererseits kodieren formale Beweisbibliotheken (z. B. die mathlib von Lean) und interaktive Theorembeweiser (ITPs) maschinenverifizierbare Mathematik als formal geprüfte Objekte. Obwohl diese Ökosysteme komplementär sind, bleiben sie entkoppelt: Bibliographische Systeme geben nicht an, ob Ergebnisse formalisiert wurden, und formale Bibliotheken sind eher um interne Abhängigkeitsgrafen als um Publikationsmetadaten organisiert. Zwar existieren „Alignment-Artefakte“ (wie Survey-Artikel oder Dokumentationen), die klassische Resultate mit formalisierten Entwicklungen verknüpft, doch diese Abbildungen sind fragmentiert, nicht standardisiert und nicht systematisch in eine abfragbare Schicht integriert.

Methodik
Das Paper schlägt eine relationale Brücken-Datenbank vor, die darauf ausgelegt ist, diese bestehenden Infrastrukturen zu integrieren, ohne sie zu ersetzen. Die Kernmethodik umfasst drei Komponenten:

1. Architektonische Integration: Das System fungiert als Alignment-Infrastruktur, die bibliographische Datensätze (aus MathSciNet und zbMATH Open) mit formalen Artefakten (aus Lean, Reservoir etc.) verknüpft. Es führt keine neue Peer-Review oder formale Verifizierung durch, sondern dient als Archivierungsplattform, die Korrespondenzen zwischen Publikationen und formalem Code aufzeichnet.
2. Formalisierungs-Score ($S(P_i)$): Die Autoren definieren eine quantitative Metrik, um das Ausmaß der Formalisierung eines spezifischen Papers $P_i$ zu messen.
   • Das Paper wird als eine Sammlung mathematischer Aussagen $S_i$ (Definitionen, Lemmata, Theoreme, Vermutungen etc.) behandelt.
   • Jedem Statement $s$ wird ein binärer Indikator $\phi(s)$ zugewiesen: 1, falls in Lean vollständig formalisiert, 0 andernfalls.
   • Unterscheidung in Anforderungen:
     • Reine Aussagen (Definitionen, Konstruktionen, Vermutungen) erfordern lediglich die Existenz des formalen Objekts.
     • Bewiesene Aussagen (Theoreme, Lemmata) erfordern sowohl die formale Aussage als auch einen vollständigen formalen Beweis.
   • Der Score wird berechnet als: $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$.
3. Machbarkeitsstudie mittels Cross-Dokument-Alignment: Um zu demonstrieren, dass diese Scores in großem Maßstab geschätzt werden können, nutzten die Autoren Large Language Models (LLMs) in einem Zero-Shot-Setting. Das Modell wurde angewiesen, ein informelles mathematisches Paper (PDF 1) mit einem Formalisierungsdokument oder einer Lean-Implementierung (PDF 2) zu vergleichen. Das Modell wurde instruiert:
   • Granulare mathematische Aussagen aus dem informellen Text zu extrahieren.
   • Diese als „Rein“ (Pure) oder „Bewiesen“ (Proved) zu klassifizieren.
   • Semantische Korrespondenzen im formalen Text zu identifizieren.
   • Den Formalisierungs-Score basierend auf dem Verhältnis der übereinstimmenden Aussagen zu berechnen.

Wesentliche Beiträge

• Interoperabilitäts-Layer: Ein Vorschlag für eine Datenbank, die bibliographische Register mit formalen Verifizierungsumgebungen vereinigt und Publikationsmetadaten mit formalen Coderepositories verknüpft.
• Definition des Formalisierungs-Scores: Eine rigorose Metrik auf Paper-Ebene ($S(P_i)$), die die Abdeckung einer Publikation innerhalb formaler Systeme quantifiziert und dabei zwischen der Existenz von Definitionen und dem Vorhandensein von Beweisen unterscheidet.
• Nachweis der Machbarkeit: Eine Proof-of-Concept-Studie, die zeigt, dass LLMs diese Scores erfolgreich schätzen können, indem sie informelle Texte mit formalen Artefakten abgleichen, was eine groß angelegte Analyse der Formalisierungsabdeckung ermöglicht.

Experimentelle Ergebnisse
Die Autoren führten Experimente mit sechs mathematischen Papern unter Verwendung von Google Gemini ohne Fine-Tuning durch. Die Ergebnisse demonstrierten die Fähigkeit des Systems, unterschiedliche Grade der Formalisierung zu unterscheiden:

• Hohe Abdeckung: Das Kugelpackungsproblem in Dimension 8 erhielt einen Score von 100, was eine vollständige Formalisierung anzeigt.
• Teilweise Abdeckung: Arbeiten zur Irrationalität von $\zeta(3)$ und zu mehrfach graduierten Proj-Schemata erhielten Scores von 50 und 67,74 (sowie 96,30 in einem zweiten Experiment), was eine substanzielle, aber unvollständige Formalisierung widerspiegelt.
• Geringe/Keine Abdeckung: Ein Paper über „Dilatations of categories“ erhielt 41,67, und ein Survey über „Algebraic magnetism“ (welcher keine Lean-Implementierung besaß) erhielt 0, als er mit nicht verwandter Dokumentation abgeglichen wurde.
  Die Experimente bestätigten, dass das Modell korrekt identifizieren konnte, wenn keine relevante Formalisierung existierte, und zwischen vollständig und teilweise formalisierten Werken differenzieren konnte.

Bedeutung und Ansprüche
Das Paper positioniert diese Arbeit als einen ersten Schritt zur Integration bibliographischer und formaler mathematischer Ökosysteme in skalierbare, maschinenlesbare Wissensgraphen. Die Autoren betonen explizit, dass das vorgeschlagene System kein Ersatz für bestehende Publikations- oder Verifizierungs-Infrastrukturen ist. Stattdessen dient es als „konnektive Schicht“, die bestehendes, informelles Alignment-Wissen in eine strukturierte, abfragbare Ressource systematisiert.

Die Bedeutung liegt in der Fähigkeit:

1. Einen einheitlichen Zugang zu veröffentlichten Resultaten und deren formalen Gegenstücken zu bieten.
2. Eine groß angelegte Analyse darüber zu ermöglichen, wie viel der mathematischen Literatur formalisiert wurde.
3. Ein Fundament für die Verknüpfung von Publikationen mit formalen Beweisobjekten zu schaffen, was potenziell KI-generierte Mathematik und Mensch-KI-Hybrid-Workflows unterstützt.

Die Autoren räumen Einschränkungen ein und merken an, dass das PDF-Parsing Ambiguitäten einführt, die Retrieval-Qualität die Genauigkeit der Scoring-Verfahren beeinflusst und LLMs spurlose Korrespondenzen erzeugen können. Folglich rahmen sie das System als ein „Best-Effort-Framework“ für relationales Alignment ein und nicht als eine perfekt getreue Abbildung, mit der Erwartung, dass Hyperlinks und Zuordnungen schließlich manuell kuratiert oder über supervidierte Prozesse – ähnlich der aktuellen bibliographischen Praxis – erstellt werden.