🔢 mathematics

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

Dit artikel presenteert een volledig geformaliseerd bewijs in Lean 4 dat de octonaire dekkingwaarde $K_8(4, 2)$ gelijk is aan 23, waarbij de bovengrens wordt vastgesteld via een expliciete code van 23 woorden en de ondergrens door het combineren van vezel-telfactoren met door LRAT weerlegde CNF-instanties om aan te tonen dat er geen dekking van 22 woorden kan bestaan.

Oorspronkelijke auteurs: Andreas Florath

Gepubliceerd 2026-06-16

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Andreas Florath

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een set speciale "veiligheidsnetten" probeert in te pakken in een gigantische, vierdimensionale kamer gevuld met miljoenen punten. Het doel is om ervoor te zorgen dat elk afzonderlijk punt in de kamer binnen een korte afstand (laten we zeggen, twee stappen) van ten minste één veiligheidsnet ligt.

De vraag die wiskundigen zich hebben gesteld is: Wat is het absolute minimale aantal veiligheidsnetten dat je nodig hebt om de hele kamer te dekken?

Voor een specifiek type kamer (waarbij elke dimensie 8 mogelijke waarden heeft), is het antwoord teruggebracht tot een zeer kleine marge: het is ofwel 22 netten of 23 netten. Dit artikel, geschreven door Andreas Florath, bewijst definitief dat 23 het magische getal is. Je kunt het niet met 22 netten.

Hier is hoe het bewijs werkt, uitgelegd aan de hand van eenvoudige analogieën:

1. Het tweeledige bewijs

Om te bewijzen dat het antwoord precies 23 is, moest de auteur twee dingen doen, zoals bewijzen dat een deur aan beide kanten op slot zit:

De bovengrens (Laten zien dat 23 werkt): De auteur heeft simpelweg een specifieke lijst van 23 veiligheidsnetten gevonden en deze gecontroleerd tegen elk punt in de kamer. Het is als zeggen: "Hier is een kaart van 23 brandweerkazernes; ik heb elke straat gelopen en bevestigd dat geen enkel huis meer dan twee blokken verwijderd is van een kazerne." Dit deel is gemakkelijk te verifiëren omdat de auteur simpelweg de lijst heeft getoond.
De ondergrens (Laten zien dat 22 faalt): Dit is het moeilijke deel. De auteur moest bewijzen dat het onmogelijk is om de kamer te dekken met slechts 22 netten. Je kunt niet simpelweg elke mogelijke rangschikking van 22 netten controleren, want er zijn er te veel (meer dan de atomen in het universum). In plaats daarvan gebruikte de auteur een slimme logische truc om aan te tonen dat elk poging om 22 netten te gebruiken onvermijdelijk een gat zal achterlaten.

2. Het detectivewerk van de "Ontbrekende Paren"

Om te bewijzen dat 22 netten niet genoeg zijn, keek de auteur niet direct naar de netten. In plaats daarvan keek de auteur naar wat er ontbrak.

Stel je voor dat de kamer een gigantisch rooster is. Als je een willekeurig paar coördinaten kiest (zoals "vloer" en "wand"), kun je kijken naar alle paren waarden die in de netten voorkomen.

De Logica: Als een specifiek paar waarden (bijv. "Vloer 3, Wand 5") nooit samen voorkomt in een van je 22 netten, dan is dat een "ontbrekend paar".
De Graaf: De auteur tekende een kaart (een graaf) voor elk paar coördinaten, waarbij de "ontbrekende" combinaties werden gemarkeerd.
De Tegenstrijdigheid: Het bewijs laat zien dat als je slechts 22 netten hebt, de regels van de geometrie deze "ontbrekende paar"-kaarten dwingen om een specifieke, verboden vorm aan te nemen: een "clique" (een strak geknoopte verbinding van ontbrekende verbindingen). Maar als die vorm bestaat, betekent dit dat er een punt in de kamer is dat te ver weg is van al je netten. Daarom kunnen 22 netten de kamer niet dekken.

3. Het "Blok" Puzzelstuk

Wanneer de auteur de situatie analyseerde waarin iemand probeert precies 22 netten te gebruiken, ontdekte hij dat de netten zich in een zeer rigide, blokachtige structuur zouden moeten rangschikken (specifiek een 3 + 3 + 2 patroon).

Denk hierbij aan het proberen te bouwen van een muur met 22 bakstenen. De wiskunde laat zien dat om gaten te vermijden, de stenen in drie specifieke groepen gestapeld zouden moeten worden. Echter, wanneer je probeert het laatste deel van de muur te bouwen met de resterende stenen, stort de geometrie in. Het is als het proberen te passen van een vierkante pen in een rond gat; de structuur die vereist is om de kamer te dekken, kan simpelweg niet bestaan met slechts 22 stukken.

4. De "Lean" Computercontrole

Dit is waar het artikel hoogtechnologisch wordt. Omdat de "ontbrekende paar"-logica het controleren van duizenden kleine mogelijkheden inhoudt (zoals een Sudoku-puzzel met miljoenen cellen), heeft de auteur een computerprogramma genaamd Lean gebruikt.

De SAT-solver: De auteur gebruikte een krachtig computerprogramma (een SAT-solver) om de enorme lijst met mogelijkheden te controleren en te zeggen: "Deze specifieke rangschikking is onmogelijk."
Het Certificaat: Meestal moeten we de computer vertrouwen. Maar hier zei de computer niet alleen "Onmogelijk". De computer produceerde ook een certificaat (een stapsgewijs bonnetje van zijn logica).
De Verificatie: Het Lean-programma las vervolgens dat bonnetje en verifieerde elke stap van de logica van de computer zelf. Dit betekent dat het bewijs machine-gecontroleerd is. We hoeven de computer niet te vertrouwen; we hoeven alleen de Lean-software te vertrouwen in haar vermogen om het bonnetje te lezen, wat veel kleiner en gemakkelijker te verifiëren is.

Samenvatting

Het artikel bewijst dat voor deze specifieke vierdimensionale kamer met 8 opties per dimensie:

23 netten zijn voldoende (hier is de lijst).
22 netten zijn niet genoeg (hier is een logisch bewijs dat elke poging om 22 netten te gebruiken een onvermijdelijke kloof creëert).

Het resultaat is een "Lean-gecertificeerd" bewijs, wat betekent dat het volledige argument — van de grote logica tot de kleinste computercontroles — is geverifieerd door een formeel wiskundig softwaresysteem, waardoor er geen ruimte is voor menselijke fouten of twijfel. Het antwoord is exact 23.

Technische Samenvatting: Een Lean-gecertificeerd bewijs van $K_8(4,2) = 23$

Probleemstelling
Het artikel behandelt de bepaling van het exacte dekkinggetal $K_q(n,r)$ , gedefinieerd als de minimale grootte van een radius- $r$ dekkingscode in de $q$ -aire Hamming-ruimte van lengte $n$ . Specifiek lost het de waarde op voor het octonaire geval met lengte 4 en radius 2: $K_8(4,2)$ . Voorafgaand aan dit werk plaatsten bestaande grenzen (specifiek de tabellen van Kéri) deze waarde in het interval $[22, 23]$ . De ondergrens werd afgeleid van de Rodemich rook-domein grens, terwijl de bovengrens werd ondersteund door large-alphabet grenzen. Het doel was om dit interval te sluiten door de ondergrens $K_8(4,2) \ge 23$ te bewijzen.

Methodologie
Het bewijs is geformaliseerd in de Lean 4 theorem prover met behulp van de mathlib bibliotheek. Het maakt gebruik van een "proof-carrying" benadering waarbij het resultaat wordt vastgesteld via twee onafhankelijke certificaten: een expliciete bovengrens en een structurele ondergrens.

Bovengrens ( $K_8(4,2) \le 23$ ):
De auteurs bieden een expliciete code aan die bestaat uit 23 codewoorden in $(\text{Fin } 8)^4$ . Het formele bewijs verifieert twee condities: de kardinaliteit van de verzameling is maximaal 23, en elk woord in de omringende ruimte (4096 woorden) bevindt zich binnen Hamming-afstand 2 van ten minste één codewoord. Dit is een uitputtende eindige controle.
Ondergrens ( $K_8(4,2) \ge 23$ ):
De kern van het artikel is een structureel non-existentie-argument voor elke hypothetische dekking $C^*$ met $|C^*| \le 22$ . Het bewijs verloopt via een sequentie van reducties:
- Fiber Counting: Voor een hypothetische dekking definiëren de auteurs "fibers" $C^*_{i,a}$ (codewoorden met symbool $a$ op coördinaat $i$ ). Ze bewijzen dat elke fiber ten minste twee codewoorden moet bevatten. Dit stelt een basislijn vast van 16 codewoorden ( $8 \text{ symbolen} \times 2$ ) per coördinaat, waardoor een "budget" overblijft van maximaal 6 excessieve codewoorden voor het geval $|C^*|=22$ (of 5 voor $|C^*| \le 21$ ).
- Missing-Pair Graphs: Het bewijs verschuift naar een "inverse" viewpoint, waarbij wordt geanalyseerd welke paren symbolen ontbreken uit de projecties van de code op coördinatenparen. Deze ontbrekende paren vormen grafen $E_{ij}$ .
- Geval $|C^*| \le 21$ : Gebruikmakend van het kleine excessieve budget, demonstreren de auteurs via combinatorische telling dat de missing-pair grafen een "simultane vierpartiete kliek" moeten bevatten (een verzameling van vier symbolen $a,b,c,d$ waarvoor alle zes de coördinaatparen ontbreken). Lemma 7 bewijst dat een dergelijke kliek niet kan bestaan in een geldige radius-2 dekking, waarmee covers van grootte 21 of minder worden uitgesloten.
- Geval $|C^*| = 22$ : Voor het resterende geval reduceert het bewijs het probleem tot een eindige classificatie van het "profiel" van de missing-pair grafen. De auteurs tonen aan dat elk geldig profiel een specifieke "gemeenschappelijke $3+3+2$ blokstructuur" moet vertonen.
- SAT/LRAT Integratie: De classificatie van deze profielen is te groot voor handmatige enumeratie. De auteurs coderen de constraints (rij/kolom graad bounds en de no-clique conditie) in Conjunctive Normal Form (CNF) instanties. Ze gebruiken een onbetrouwbare SAT-solver om Linear RAT (LRAT) refutaties (bewijzen van onbevredigbaarheid) te genereren.
- Formele Verificatie: Lean parseert deze LRAT-certificaten en speelt de refutaties mechanisch opnieuw af om te bewijzen dat er geen geldige profielen bestaan voor een 22-woord cover.
- Finale Contradictie: Zelfs als een gemeenschappelijke blokstructuur zou worden aangenomen, leiden de auteurs een contradictie af in de "2-symbool component" van de structuur. Deze component zou een binaire strength-2 array van lengte 4 vereisen met ten hoogste 4 rijen, wat wiskundig onmogelijk is.

Belangrijkste Bijdragen

Exacte Waarde: Het artikel stelt de exacte waarde $K_8(4,2) = 23$ vast, waarmee het eerder bekende interval $[22, 23]$ wordt gesloten.
Geformaliseerde Ondergrens: Het biedt een volledig geformaliseerd bewijs in Lean 4 dat alle 22-woord covers uitsluit. Dit wordt bereikt, niet door volume-argumenten, maar door structurele obstructies afgeleid van fiber counts en missing-pair grafen.
Proof-Carrying Artifact: Het resultaat is verpakt als een Lean-artifact die de expliciete code, de structurele lemma's, de CNF-instanties en de LRAT-refutaties bevat. Cruciaal is dat de SAT-solver niet deel uitmaakt van de trusted computing base; Lean verifieert de LRAT-certificaten intern.
Patroon voor Computationele Ondergrenzen: Het artikel introduceert een herbruikbaar patroon voor het koppelen van door een solver geproduceerd bewijs aan dekking-code ondergrenzen. Het scheidt de "ontdekking" (onbetrouwbare solver) van de "verificatie" (vertrouwde Lean kernel), waardoor grote eindige classificatieproblemen computationeel kunnen worden opgelost terwijl de formele correctheid behouden blijft.

Resultaten
Het primaire resultaat is de stelling $K_8(4,2) = 23$ .

Bovengrens: Bewezen door een expliciete 23-woord code.
Ondergrens: Bewezen door aan te tonen dat een cover van grootte 22 leidt tot een contradictie via een gedwongen "gemeenschappelijk $3+3+2$ blok systeem", wat een onmogelijke binaire array impliceert.
Prestaties: De formele verificatie vereist aanzienlijke computationele middelen. Het kernel-mode replay van het hoofd-bewijsbestand vereiste ongeveer 143 GiB RAM, terwijl native mode dit reduceerde tot ongeveer 5,5 GiB. De LRAT checking fase duurde ongeveer 17 minuten in kernel mode.

Betekenis en Claims
Het artikel claimt primair betekenis in het domein van de geformaliseerde wiskunde en de methodologie van het combineren van combinatorische redenering met computationele certificaten.

Methodologische Verschuiving: Het demonstreert dat structurele combinatoriek gecombineerd kan worden met "proof-carrying" computationele bewijslast. De SAT-solver wordt gebruikt om eindige obstructies te ontdekken, maar de wiskundige brug en de verificatie van de output van de solver worden volledig door de theorem prover afgehandeld.
Vertrouwensgrens: Het werk verheldert de vertrouwensgrens in formele bewijzen die betrokken zijn bij SAT-solvers. De solver is onbetrouwbaar; de Lean kernel controleert de LRAT-certificaten en de logische deductie die deze certificaten verbindt met de dekking-code stelling.
Schaalbaarheid: Het resultaat dient als een testcase voor het afhandelen van covering-code problemen die te groot zijn voor handmatig bewijs, maar klein genoeg zijn voor reductie tot eindige classificatieproblemen die oplosbaar zijn via SAT-solvers.
Geen Nieuwe Toepassingen: Het artikel claimt geen nieuwe toepassingen voor de waarde $K_8(4,2)=23$ zelf, noch stelt het nieuwe experimentele protocollen voor. De bijdrage is strikt de resolutie van een specifiek openstaand probleem in coding theory tabellen en de demonstratie van een formele verificatieworkflow voor dergelijke problemen.