🔢 mathematics

A Lean-Certified Proof of $K_8(4, 2) = 23$

Diese Arbeit präsentiert einen vollständig formalisierten Beweis in Lean 4, dass der oktonäre Überdeckungswert $K_8(4, 2)$ gleich 23 ist, wobei die obere Schranke durch einen expliziten 23-Wort-Code und die untere Schranke durch die Kombination von Fasernzählung-Argumenten mit LRAT-widerlegten CNF-Instanzen etabliert wird, um zu zeigen, dass keine 22-Wort-Überdeckung existieren kann.

Ursprüngliche Autoren: Andreas Florath

Veröffentlicht 2026-06-16

📖 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, eine Reihe spezieller „Sicherheitsnetze“ in einen riesigen, vierdimensionalen Raum zu packen, der mit Millionen von Punkten gefüllt ist. Das Ziel ist es, sicherzustellen, dass jeder einzelne Punkt im Raum innerhalb einer kurzen Distanz (sagen wir, zwei Schritte) zu mindestens einem Sicherheitsnetz liegt.

Die Frage, die sich Mathematiker gestellt haben, lautet: Was ist die absolute Mindestanzahl an Sicherheitsnetzen, die man benötigt, um den gesamten Raum abzudecken?

Für eine spezifische Art von Raum (bei dem jede Dimension 8 mögliche Werte hat) wurde die Antwort auf einen winzigen Bereich eingegrenzt: Es sind entweder 22 oder 23 Netze. Dieses Paper, geschrieben von Andreas Florath, beweist definitiv, dass 23 die magische Zahl ist. Mit 22 kann man es nicht schaffen.

Hier ist die Funktionsweise des Beweises, heruntergebrochen in einfache Analogien:

1. Der zweiteilige Beweis

Um zu beweisen, dass die Antwort genau 23 ist, musste der Autor zwei Dinge tun, so wie man beweisen muss, dass eine Tür von beiden Seiten verriegelt ist:

Die obere Schranke (Zeigen, dass 23 funktioniert): Der Autor fand einfach eine spezifische Liste von 23 Sicherheitsnetzen und prüfte sie gegen jeden einzelnen Punkt im Raum. Es ist, als würde man sagen: „Hier ist eine Karte von 23 Feuerstationen; ich bin jede Straße abgegangen und habe bestätigt, dass kein Haus mehr als zwei Häuserblocks von einer Station entfernt ist.“ Dieser Teil ist leicht zu verifizieren, da der Autor einfach die Liste vorgelegt hat.
Die untere Schranke (Zeigen, dass 22 scheitert): Dies ist der schwierige Teil. Der Autor musste beweisen, dass es unmöglich ist, den Raum mit nur 22 Netzen abzudecken. Man kann nicht einfach jede mögliche Anordnung von 22 Netzen prüfen, denn es gibt zu viele (mehr als es Atome im Universum gibt). Stattdessen nutzte der Autor einen cleveren Logiktrick, um zu zeigen, dass jeder Versuch mit 22 Netzen unweigerlich eine Lücke hinterlassen würde.

2. Die Detektivarbeit der „fehlenden Paare“

Um zu beweisen, dass 22 Netze nicht ausreichen, hat der Autor nicht die Netze direkt betrachtet. Stattdessen hat er sich das angesehen, was fehlte.

Stellen Sie sich den Raum als ein riesiges Gitter vor. Wenn Sie zwei Koordinaten wählen (wie „Boden“ und „Wand“), können Sie alle Paare von Werten betrachten, die in den Netzen vorkommen.

Die Logik: Wenn ein bestimmtes Paar von Werten (z. B. „Boden 3, Wand 5“) niemals zusammen in einem Ihrer 22 Netze auftaucht, dann ist das ein „fehlendes Paar“.
Der Graph: Der Autor zeichnete eine Karte (einen Graphen) für jedes Paar von Koordinaten und markierte die „fehlenden“ Kombinationen.
Der Widerspruch: Der Beweis zeigt, dass, wenn man nur 22 Netze hat, die Regeln der Geometrie diese „fehlenden Paar“-Karten dazu zwingen, eine bestimmte, verbotene Form zu bilden – einen „Clique“ (einen engen Knoten fehlender Verbindungen). Aber wenn diese Form existiert, bedeutet das, dass es einen Punkt im Raum gibt, der zu weit von jedem Ihrer Netze entfernt ist. Daher können 22 Netze den Raum nicht abdecken.

3. Das „Block“-Puzzle

Als der Autor den Fall analysierte, in dem jemand versucht, genau 22 Netze zu verwenden, stellte er fest, dass die Netze sich in einer sehr starren, blockartigen Struktur (speziell einem 3 + 3 + 2 Muster) anordnen müssten.

Denken Sie daran wie beim Versuch, eine Mauer mit 22 Ziegeln zu bauen. Die Mathematik zeigt, dass die Ziegel, um Löcher zu vermeiden, in drei spezifischen Gruppen gestapelt werden müssten. Wenn man jedoch versucht, den letzten Abschnitt der Mauer mit den verbleibenden Ziegeln zu bauen, bricht die Geometrie zusammen. Es ist wie der Versuch, einen quadratischen Stein in ein rundes Loch zu passen; die Struktur, die erforderlich ist, um den Raum abzudecken, kann mit nur 22 Teilen schlichtweg nicht existieren.

4. Der „schlanke“ Computer-Check

Hier wird das Paper hochtechnologisch. Da die „fehlende Paar“-Logik die Überprüfung tausender winziger Möglichkeiten beinhaltet (wie ein Sudoku-Rätsel mit Millionen von Zellen), nutzte der Autor ein Computerprogramm namens Lean.

Der SAT-Solver: Der Autor nutzte ein leistungsstarkes Computerprogramm (einen SAT-Solver), um die massive Liste der Möglichkeiten zu prüfen und zu sagen: „Diese spezifische Anordnung ist unmöglich.“
Das Zertifikat: Normalerweise müssen wir dem Computer vertrauen. Aber hier hat der Computer nicht nur gesagt: „Unmöglich“. Er produzierte ein Zertifikat (einen Schritt-für-Schritt-Beleg seiner Logik).
Die Verifizierung: Das Lean-Programm hat diesen Beleg dann gelesen und jeden einzelnen Schritt der Logik des Computers selbst verifiziert. Das bedeutet, der Beweis ist maschinengeprüft. Wir müssen nicht dem „Gehirn“ des Computers vertrauen, sondern nur der Fähigkeit des Lean-Programms, den Beleg zu lesen, der viel kleiner und einfacher zu verifizieren ist.

Zusammenfassung

Das Paper beweist, dass für diesen spezifischen vierdimensionalen Raum mit 8 Optionen pro Dimension gilt:

23 Netze sind ausreichend (hier ist die Liste).
22 Netze sind nicht ausreichend (hier ist ein logischer Beweis, dass jeder Versuch, 22 Netze zu verwenden, eine unvermeidliche Lücke erzeugt).

Das Ergebnis ist ein „Lean-zertifizierter“ Beweis, was bedeutet, dass das gesamte Argument – von der großen Logik bis hin zu den winzigen Computerprüfungen – durch ein formales mathematisches Softwaresystem verifiziert wurde, sodass kein Raum für menschliche Fehler oder Zweifel bleibt. Die Antwort ist exakt 23.

Technisches Resümee: Ein Lean-zertifizierter Beweis für $K_8(4,2) = 23$

Problemstellung
Die Arbeit befasst sich mit der Bestimmung der exakten Abdeckungsgrenze $K_q(n,r)$ , definiert als die minimale Größe eines Radius- $r$ Abdeckcodes im $q$ -ären Hamming-Raum der Länge $n$ . Insbesondere löst sie den Wert für den oktonären Fall mit Länge 4 und Radius 2: $K_8(4,2)$ . Vor dieser Arbeit platzierten bestehende Schranken (speziell Kéris Tabellen) diesen Wert im Intervall $[22, 23]$ . Die untere Schranke wurde aus der Rodemich-Rook-Domain-Schranke abgeleitet, während die obere Schranke durch Large-Alphabet-Schranken gestützt wurde. Das Ziel war es, dieses Intervall zu schließen, indem bewiesen wird, dass $K_8(4,2) \ge 23$ gilt.

Methodik
Der Beweis ist im Lean 4 Theorem Prover unter Verwendung der mathlib-Bibliothek formalisiert. Er verwendet einen „beweisführenden“ Ansatz, bei dem das Ergebnis durch zwei unabhängige Zertifikate etabliert wird: eine explizite obere Schranke und eine strukturelle untere Schranke.

Obere Schranke ( $K_8(4,2) \le 23$ ):
Die Autoren liefern einen expliziten Code, der aus 23 Codewörtern in $(\text{Fin } 8)^4$ besteht. Der formale Beweis verifiziert zwei Bedingungen: die Kardinalität der Menge beträgt höchstens 23, und jedes Wort im umgebenden Raum (4096 Wörter) liegt innerhalb der Hamming-Distanz 2 von mindestens einem Codewort. Dies ist eine erschöpfende endliche Prüfung.
Untere Schranke ( $K_8(4,2) \ge 23$ ):
Der Kern der Arbeit ist ein strukturelles Nichtexistenzargument für jeden hypothetischen Cover $C^*$ mit $|C^*| \le 22$ . Der Beweis erfolgt durch eine Sequenz von Reduktionen:
- Faser-Zählung (Fiber Counting): Für einen hypothetischen Cover definieren die Autoren „Fasern“ $C^*_{i,a}$ (Codewörter mit dem Symbol $a$ an Koordinate $i$ ). Sie beweisen, dass jede Faser mindestens zwei Codewörter enthalten muss. Dies etabliert eine Basis von 16 Codewörtern ( $8 \text{ Symbole} \times 2$ ) pro Koordinate, wodurch ein „Budget“ von höchstens 6 überschüssigen Codewörtern für den Fall $|C^*|=22$ (oder 5 für $|C^*| \le 21$ ) verbleibt.
- Fehlende-Paar-Graphen (Missing-Pair Graphs): Der Beweis wechselt zu einer „inversen“ Sichtweise und analysiert, welche Paare von Symbolen aus den Projektionen des Codes auf Koordinatenpaare fehlen. Diese fehlenden Paare bilden Graphen $E_{ij}$ .
- Fall $|C^*| \le 21$ : Unter Verwendung des geringen überschüssigen Budgets zeigen die Autoren mittels kombinatorischer Zählung, dass die fehlenden-Paar-Graphen eine „simultane viergeteilte Clique“ (eine Menge von vier Symbolen $a,b,c,d$ , bei denen alle sechs Koordinatenpaare fehlen) enthalten müssen. Lemma 7 beweist, dass eine solche Clique in einem gültigen Radius-2-Cover nicht existieren kann, und schließt somit Cover der Größe 21 oder kleiner aus.
- Fall $|C^*| = 22$ : Für den verbleibenden Fall reduziert der Beweis das Problem auf eine endliche Klassifizierung des „Profils“ der fehlenden-Paar-Graphen. Die Autoren zeigen, dass jeder gültige Profil eine spezifische „gemeinsame $3+3+2$ Blockstruktur“ aufweisen muss.
- SAT/LRAT-Integration: Die Klassifizierung dieser Profile ist für eine manuelle Enumeration zu groß. Die Autoren kodieren die Constraints (Zeilen-/Spalten-Grad-Schranken und die No-Clique-Bedingung) in Konjunktive Normalformen (CNF-Instanzen). Sie verwenden einen nicht vertrauenswürdigen SAT-Solver, um Linear RAT (LRAT) Refutationen (Beweise der Unerfüllbarkeit) zu generieren.
- Formale Verifikation: Lean parst diese LRAT-Zertifikate und spielt die Refutationen mechanisch nach, um zu beweisen, dass kein gültiges Profil für einen 22-Wort-Cover existiert.
- Endgültiger Widerspruch: Selbst wenn eine gemeinsame Blockstruktur angenommen würde, leiten die Autoren einen Widerspruch in der „2-Symbol-Komponente“ dieser Struktur her. Diese Komponente würde ein binäres Stärke-2-Array der Länge 4 mit höchstens 4 Zeilen erfordern, was mathematisch unmöglich ist.

Wesentliche Beiträge

Exakter Wert: Die Arbeit etabliert den exakten Wert $K_8(4,2) = 23$ und schließt das zuvor bekannte Intervall $[22, 23]$ .
Formalisierter unterer Grenzwert: Sie liefert einen vollständig formalisierten Beweis in Lean 4, der alle 22-Wort-Cover ausschließt. Dies wird nicht durch Volumenargumente, sondern durch strukturelle Hindernisse erreicht, die aus Faserzählungen und fehlenden-Paar-Graphen abgeleitet sind.
Beweisführendes Artefakt: Das Ergebnis wird als Lean-Artefakt verpackt, das den expliziten Code, die strukturellen Lemmata, die CNF-Instanzen und die LRAT-Refutationen enthält. Entscheidend ist, dass der SAT-Solver nicht Teil der vertrauenswürdigen Rechenbasis (Trusted Computing Base) ist; Lean verifiziert die LRAT-Zertifikate intern.
Muster für computergestützte untere Schranken: Die Arbeit führt ein wiederverwendbares Muster zur Anbindung von Solver-produzierten Evidenzen an Abdeckungsgrenzen ein. Sie trennt die „Entdeckung“ (unvertrauenswürdiger Solver) von der „Verifikation“ (vertrauenswürdiger Lean-Kernel), wodurch große endliche Klassifizierungsprobleme computergestützt gelöst werden können, während die formale Korrektheit gewahrt bleibt.

Ergebnisse
Das primäre Ergebnis ist der Satz $K_8(4,2) = 23$ .

Obere Schranke: Bewiesen durch einen expliziten 23-Wort-Code.
Untere Schranke: Bewiesen durch den Nachweis, dass ein 22-Wort-Cover zu einem Widerspruch führt, der durch ein erzwungenes „gemeinsames $3+3+2$ Blocksystem“ impliziert wird, welches ein unmögliches binäres Array zur Folge hat.
Performance: Die formale Verifikation beansprucht erhebliche Rechenressourcen. Das Replay der Hauptbeweisdatei im Kernel-Modus erforderte etwa 143 GiB RAM, während der Native-Modus diesen Bedarf auf etwa 5,5 GiB reduzierte. Die Phase der LRAT-Prüfung dauerte im Kernel-Modus etwa 17 Minuten.

Bedeutung und Ansprüche
Die Arbeit beansprucht Bedeutung primär im Bereich der formalisierten Mathematik und der Methodik der Kombination von kombinatorischer Argumentation mit computergestützten Zertifikaten.

Methodologischer Wandel: Sie zeigt, dass strukturelle Kombinatorik mit „beweisführenden“ computergestützten Evidenzen kombiniert werden kann. Der SAT-Solver wird genutzt, um endliche Hindernisse zu entdecken, aber die mathematische Brücke und die Verifikation der Ausgabe des Solvers werden vollständig durch den Theorem Prover gehandhabt.
Vertrauensgrenze: Die Arbeit klärt die Vertrauensgrenze in formalen Beweisen, die SAT-Solver involvieren. Der Solver ist nicht vertrauenswürdig; der Lean-Kernel prüft die LRAT-Zertifikate und die logische Deduktion, die diese Zertifikate mit der Aussage über den Abdeckcode verbindet.
Skalierbarkeit: Das Ergebnis dient als Testfall für die Handhabung von Abdeckungsproblemen, die zu groß für einen manuellen Beweis, aber klein genug für eine durch SAT-Solver lösbare endliche Klassifizierung sind.
Keine neuen Anwendungen: Die Arbeit erhebt keine Ansprüche auf neue Anwendungen für den Wert $K_8(4,2)=23$ selbst und schlägt auch keine neuen experimentellen Protokolle vor. Ihr Beitrag liegt strikt in der Lösung eines spezifischen offenen Problems in den Tabellen der Kodierungstheorie und der Demonstration eines formalen Verifikations-Workflows für solche Probleme.