LeanGeo: Formalisierung geometrischer Wettbewerbsaufgaben in Lean

Geometrieaufgaben stellen eine zentrale Testplattform für die Rechenfähigkeiten von KI-Systemen dar. Bisher können die meisten automatischen Lösungswerkzeuge Probleme nicht in einem einheitlichen Rahmen formulieren, was die Integration mit anderen mathematischen Bereichen erschwert. Zudem sind geometrische Beweise häufig diagrammabhängig, was deren formale Verifikation besonders schwierig macht.

Mit LeanGeo wird dieses Problem angegangen: Es handelt sich um ein einheitliches, formales System, das geometrische Wettbewerbsaufgaben innerhalb des Lean‑4 Theorem Provers formalisiert und löst. Die Bibliothek enthält eine umfangreiche Sammlung hochrangiger geometrischer Sätze, die auf Leans Grundlagenlogik aufbauen. Dadurch lassen sich Beweise rigoros verifizieren und nahtlos mit der bestehenden Mathlib‑Bibliothek verbinden.

Zur Bewertung der aktuellen KI‑Technologien wurde LeanGeo‑Bench entwickelt – ein Benchmark aus geometrischen Aufgaben der Internationalen Mathematik-Olympiade (IMO) und weiteren anspruchsvollen Quellen. Die Ergebnisse zeigen, welche Stärken und Schwächen moderne Large‑Language‑Models bei der geometrischen Problemlösung aufweisen und unterstreichen den Bedarf an weiteren Fortschritten im automatisierten geometrischen Denken.

Die komplette Theorem‑Bibliothek sowie das Benchmark‑Set sind als Open‑Source-Projekt auf GitHub verfügbar: https://github.com/project-numina/LeanGeo/tree/master.