🔢 mathematics

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

Diese Arbeit präsentiert eine Formalisierung der elementaren Theorie von q-ären Covering-Codes in Lean 4 und etabliert damit eine wiederverwendbare, prüfbare Grundlage mit beweisführenden Zertifikaten zur Verifizierung von oberen und unteren Schranken für Covering-Zahlen.

Ursprüngliche Autoren: Andreas Florath

Veröffentlicht 2026-06-09

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Andreas Florath

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, ein riesiges, mehrdimensionales Schachbrett mit einer begrenzten Anzahl von „Sicherheitsnetzen“ abzudecken.

In der Welt der Mathematik ist dies das Problem der Überdeckungscodes (Covering Codes). Sie haben ein Gitter möglicher Positionen (wie ein Schachbrett, aber es könnte 3D, 4D oder sogar höherdimensional sein). Sie möchten eine kleine Anzahl von „Zentren“ auf diesem Gitter platzieren. Die Regel lautet, dass jedes einzelne Feld auf dem Brett innerhalb eines bestimmten Abstands (sagen wir, einen Schritt) von mindestens einem Ihrer Zentren liegen muss.

Die große Frage ist: Was ist die absolute minimale Anzahl an Zentren, die Sie benötigen, um das gesamte Brett abzudecken?

Dieses Paper, geschrieben von Andreas Florath, versucht nicht, einen neuen Rekord für die kleinste Anzahl an Zentren aufzustellen. Stattdessen baut es einen digitalen, unknackbaren Tresor, um zu beweisen, dass die Zahlen, die wir bereits kennen, korrekt sind.

Hier ist eine Aufschlüsselung der Ideen des Papers unter Verwendung einfacher Analogien:

1. Das „beweistragende Zertifikat“ (Das Goldene Ticket)

Normalerweise, wenn ein Mathematiker sagt: „Ich habe einen Code mit 73 Zentren gefunden, der das Brett abdeckt“, zeigt er Ihnen eine Liste von Zahlen. Sie müssen ihm vertrauen oder Stunden damit verbringen, die Mathematik selbst zu überprüfen.

Dieses Paper führt ein „beweistragendes Zertifikat“ (Proof-Carrying Certificate) ein. Betrachten Sie dies nicht nur als eine Liste von Zahlen, sondern als ein Goldenes Ticket, das mit einem eingebauten, selbstprüfenden Zaubertrick kommt.

Das Ticket: Es besagt: „Hier ist eine Menge von 73 Zentren.“
Der Zaubertrick: Das Ticket enthält einen winzigen, automatisierten Roboter (geschrieben in einer Sprache namens Lean 4), der sofort jedes einzelne Feld auf dem Brett überprüft, um zu bestätigen: „Ja, dieses Feld ist abgedeckt. Ja, dieses Feld ist abgedeckt. Ja, alle von ihnen sind es.“
Das Ergebnis: Sie müssen dem Autor nicht vertrauen. Sie führen einfach den Roboter aus. Wenn der Roboter „Pass“ sagt, ist der Beweis zu 100 % mathematisch garantiert.

2. Das „Zweiteilige Puzzle“

Um zu beweisen, dass Sie die perfekte (exakte) Anzahl an Zentren haben, müssen Sie zwei verschiedene Puzzles gleichzeitig lösen:

Die obere Schranke (Die Konstruktion): „Ich kann das Brett mit 73 Zentren abdecken.“ (Sie zeigen die Liste).
Die untere Schranke (Die unmögliche Aufgabe): „Es ist unmöglich, das Brett mit 72 Zentren abzudecken.“ (Sie beweisen, dass Sie, egal wie Sie es versuchen, immer eine Lücke lassen werden).

Dieses Paper baut ein System auf, in dem diese beiden Puzzles separate Teile sind. Man kann ein Zertifikat für die „73“ haben und ein separates Zertifikat für das „Unmöglich mit 72“. Wenn sie aufeinandertreffen, rasten sie zusammen und bilden eine perfekte, exakte Antwort.

3. Das „Lego der Mathematik“

Der Autor hat eine massive Bibliothek von Lego-Steinen (formalen Regeln) gebaut.

Einige Steine sind einfach: „Wenn Sie ein kleines Brett abdecken, können Sie ein größeres Brett abdecken, indem Sie ein paar weitere Teile hinzufügen.“
Einige Steine sind komplex: „Wenn Sie zwei verschiedene Arten von Brettern kombinieren, ändern sich die Regeln der Überdeckung genau so.“

Das Schöne an diesem Paper ist, dass diese Steine austauschbar sind. Wenn jemand anderes einen neuen Weg findet, ein Brett abzudecken, kann er seinen neuen Stein einfach in diese bestehende Lego-Struktur einrasten lassen, und das gesamte System verifiziert ihn automatisch.

4. Die „Datenbank der Wahrheit“

Das Paper enthält eine beweistragende Datenbank (Proof-Carrying Database). Stellen Sie sich ein Bibliotheksbuch vor, in dem anstatt nur die Antwort „Die Antwort ist 7“ zu drucken, das Buch eine Videoaufnahme des Beweises enthält.

Wenn Sie eine Zahl in dieser Datenbank nachschlagen, gibt sie Ihnen nicht nur eine Zahl. Sie gibt Ihnen den Trace (die schrittweise Videoaufnahme) dessen, wie diese Zahl bewiesen wurde.
Sie können dieses Video im Lean 4-System wieder abspielen, und es wird den Beweis von Grund auf neu durchlaufen, um sicherzustellen, dass er immer noch hält.

5. Das Beispiel „Fußballtippen“

Das Paper verwendet eine reale Analogie, um das Problem zu erklären: Das Fußballtippen (Football Pool).
Stellen Sie sich vor, Sie wetten auf 8 Fußballspiele. Jedes Spiel hat 3 mögliche Ausgänge (Sieg, Unentschieden, Niederlage). Sie möchten einen Satz Wettscheine kaufen.

Das Ziel: Egal was die tatsächlichen Ergebnisse sind, Sie wollen garantieren, dass mindestens einer Ihrer Wettscheine „nah dran“ ist (vielleicht nur eine Vorhersage falsch).
Die Mathematik: Wie viele Wettscheine müssen Sie kaufen, um dies zu garantieren?
Die Rolle des Papers: Das Paper nimmt eine berühmte, veröffentlichte Lösung für dieses Problem (bei der jemand eine Menge von 486 Wettscheinen gefunden hat) und verwandelt sie in ein maschinenprüfbares Zertifikat. Es beweist zweifelsfrei, dass 486 Wettscheine funktionieren.

Was dieses Paper tatsächlich behauptet (und was nicht)

Es BEHAUPTET: Es hat ein solides, wiederverwendbares Fundament (eine „formale Grundlage“) geschaffen, in dem Beweise für Überdeckungscodes gespeichert, geprüft und automatisch kombiniert werden können. Es hat mehrere spezifische, bekannte Zahlen (wie die 486 Wettscheine für das 8-Spiele-Problem) mit diesem neuen System verifiziert.
Es BEHAUPT NICHT: Es behauptet nicht, einen neuen Rekord für die kleinste Anzahl an benötigten Wettscheinen gefunden zu haben. Es behauptet nicht, das Problem für jedes mögliche Szenario gelöst zu haben. Es ist ein Werkzeug-Erstellungs-Paper, kein Rekord-brechendes Paper.

Das große Ganze

Betrachten Sie dieses Paper als den Bau eines hochsicheren Tresors für mathematische Wahrheiten. Früher mussten Sie, wenn Sie einen komplexen Überdeckungscode überprüfen wollten, einem Menschen oder einem Computerprogramm vertrauen, das einen Fehler enthalten könnte. Dank dieses Papers haben Sie nun ein System, in dem der Beweis selbst ein Stück Software ist, das Sie ausführen können, um die Wahrheit sofort zu verifizieren. Es verwandelt „Ich denke, das ist richtig“ in „Der Computer hat bewiesen, dass dies richtig ist“.

Technisches Resümee: Formale Grundlagen und beweistragende Zertifikate für q-äre Covering-Codes in Lean 4

Problemstellung
Covering-Codes in endlichen Hamming-Räumen suchen nach der kleinsten Menge von Wörtern (Codewörtern), sodass die Vereinigung ihrer Hamming-Kugeln des Radius $r$ den gesamten Raum $A^n$ abdeckt. Die zentrale Größe ist die $q$ -äre Covering-Zahl $K_q(n,r)$ , definiert als die minimale Größe eines solchen Codes. Während die Definition elementar ist, beruht die Bestimmung exakter Werte oder enger Schranken für $K_q(n,r)$ typischerweise auf einer Mischung aus expliziten Konstruktionen, Argumenten der Abzählung, rekursiven Relationen und Computersuchen. Eine wesentliche Herausforderung auf diesem Gebiet besteht darin, dass exakte Aussagen $K_q(n,r) = k$ zwei unabhängige Komponenten erfordern: eine explizite Konstruktion, die eine obere Schranke beweist ( $K_q(n,r) \le k$ ), und einen Beweis, dass kein kleinerer Code existiert (eine untere Schranke $K_q(n,r) \ge k$ ). Diese Komponenten stammen oft aus disparaten Quellen, was die Verifizierung exakter Werte schwierig macht.

Methodik
Die Arbeit präsentiert eine Formalisierung der elementaren Covering-Code-Theorie im Theorembeweiser Lean 4. Die Methodik zeichnet sich durch drei zentrale Designentscheidungen aus:

Repräsentation von Wörtern: Wörter werden als abhängige Funktionen von einem Koordinatentyp zu einem Alphabettyp modelliert. Der allgemeine $q$ -äre Hamming-Raum der Länge $n$ wird als Fin n → Fin q repräsentiert. Diese funktionale Repräsentation bewahrt eine allgemeine Schnittstelle für abstrakte Koordinatentypen, während sie die $q$ -äre Spezialisierung vereinfacht.
Zertifikatsbasierte Prädikate: Anstatt $K_q(n,r)$ $K_{q} (n, r)$ als eine nicht-berechenbare Minimierungsfunktion zu definieren, verwendet die Formalisierung logische Prädikate, um Aussagen über Covering-Zahlen darzustellen.
- KUpper r k: Behauptet die Existenz eines endlichen Covering-Codes der Größe höchstens $k$ (obere Schranke).
- KLower r k: Behauptet, dass jeder endliche Covering-Code eine Größe von mindestens $k$ hat (untere Schranke).
- KSpec r k: Kombiniert beide, um Exaktheit zu behaupten ( $K_q(n,r) = k$ ).
  Dieser modulare Ansatz ermöglicht es, obere und untere Schranken aus unterschiedlichen Quellen unabhängig voneinander zusammenzuführen.
Beweistragende Datenbank: Die Arbeit implementiert eine Datenbank, in der gespeicherte Schranken nicht bloß numerische Werte, sondern „beweistragende“ Objekte sind. Jeder Eintrag enthält einen Ableitungs-Trace. Das Abspielen dieses Traces in Lean rekonstruiert einen formalen Beweis des entsprechenden QaryKUpper- oder QaryKLower-Prädikats. Das System unterscheidet zwischen handgeschriebenen mathematischen Theoremen (kernel-geprüft) und generierten Daten (unvertrauenswürdige Produzenten, deren Output via Trace-Replay validiert wird).

Zentrale Beiträge
Die Arbeit etabliert eine wiederverwendbare, prüfbare Grundlage für maschinengeprüfte Covering-Code-Zertifikate. Ihre spezifischen Beiträge umfassen:

Formale Infrastruktur: Ein vollständiges Lean 4 Framework für endliche Hamming-Räume, Hamming-Distanz, abgeschlossene Kugeln und Covering-Prädikate, das Randfälle (z. B. $q=0$ , $n=0$ , $r \ge n$ ) rigoros innerhalb der Definitionen behandelt, statt sie als informelle Konventionen vorzubehandeln.
Analytische Ergebnisse: Formale Beweise der $q$ -ären Hamming-Kugel-Volumenformel und der klassischen Sphären-Covering-Unterschranke. Die Sphären-Covering-Schranke ist als berechenbare Funktion sphereLower gekapselt, die zertifizierte untere Schranken-Zertifikate generiert.
Strukturelle Theoreme: Formalisierung elementar exakter Fälle (z. B. $K_q(n,0) = q^n$ , $K_q(n, n-1) = q$ ) und struktureller Konstruktionen, einschließlich eines Produkt-Covering-Theorems und verschiedener Nachbarschaftsrelationen (Punktur, Verlängerung, Alphabetprojektion und Konkatenation), die Schranken zwischen Parameter-Triples transportieren.
Fallstudie (Van Laarhoven et al.): Ein End-to-End-Workflow zur Formalisierung publizierter expliziter Codes. Die Autoren transkribierten Covering-Codes aus einem Paper von Van Laarhoven et al. von 1989 in Lean und kodierten diese als gepackte Arrays, um Elaboration-Limits zu vermeiden. Das System verifizierte die Covering-Eigenschaft sowie die Kardinalität und produzierte maschinengeprüfte obere Schranken-Zertifikate für $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ und $K_3(8,1) \le 486$ .
Datenbank-Implementierung: Eine beweistragende Datenbank mit 52.822 Einträgen für die Parameter $0 \le q \le 21$ , $0 \le n \le 48$ und $0 \le r \le 48$ . Diese Datenbank enthält exakte Zertifikate für kleine Fälle (z. B. $K_2(5,1)=7$ , $K_3(3,1)=5$ ) und Intervalle, die aus dem Trace-Replay abgeleitet wurden.

Ergebnisse
Die Formalisierung verifiziert erfolgreich:

Die $q$ -äre Kugelvolumenformel und die Sphere-Covering-Unterschranke.
Elementare exakte Werte wie $K_2(5,1)=7$ , $K_2(6,2)=4$ , $K_3(3,1)=5$ und $K_4(3,1)=8$ .
Obere Schranken für das ternäre Fußballwetten-Problem, abgeleitet aus expliziten Codes, insbesondere $K_3(6,1) \le 73$ , $K_3(7,1) \le 186$ und $K_3(8,1) \le 486$ .
Eine uniforme Zwei-Block-Zyklischen-Konstruktion, die $K_q(3,1) \le \lceil q^2/2 \rceil$ beweist.

Der Prozess der Datenbank-Abschlussbildung propagierte diese primitiven Quellen erfolgreich durch zertifizierte Relationsregeln, um eine konsistente Tabelle von Schranken zu generieren. Das System unterstützt zwei Beweismodi: einen „Kernel-Modus“, der das Standard-decide für stärkere Replay-Garantien nutzt, und einen „Native-Modus“, der den kompilierten Evaluator von Lean für eine schnellere Entwicklung verwendet, wobei klare Vertrauensgrenzen für jeden Modus definiert sind.

Bedeutung und Ansprüche
Die Arbeit stellt explizit klar, dass ihr primärer Beitrag nicht die Entdeckung neuer rekordverdächtiger Schranken oder die Reproduktion bestehender Literaturtabellen ist. Stattdessen liegt ihre Bedeutung in der Bereitstellung einer formalen Schnittstelle und einer prüfbaren Grundlage für Covering-Code-Zertifikate.

Die Arbeit schließt die Lücke zwischen der klassischen Covering-Code-Literatur und zukünftigen computergestützten Zertifikaten. Durch die Trennung von oberen Schranken-Zeugen, unteren Schranken-Argumenten und Exaktheits-Prädikaten ermöglicht die Formalisierung, dass Ergebnisse aus expliziten Konstruktionen, kombinatorischer Abzählung und (potenziell) zukünftigen SAT- oder Integer-Programming-Solvern innerhalb eines einzigen vertrauenswürdigen Frameworks geprüft und kombiniert werden können. Die „beweistragende“ Natur der Datenbank stellt sicher, dass jede berichtete Schranke auf einen maschinengeprüften Beweis zurückgeführt werden kann, was die Herausforderungen der Reproduzierbarkeit und Verifizierbarkeit in diesem Bereich adressiert. Die Arbeit positioniert sich als ein grundlegender Schritt hin zu einer Zukunft, in der computergestützte Suchergebnisse nahtlos in formale mathematische Bibliotheken integriert werden können.