🔢 mathematics

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

Este artículo presenta una prueba totalmente formalizada en Lean 4 de que el valor del código de cobertura octonaria $K_8(4, 2)$ es igual a 23, estableciendo el límite superior mediante un código explícito de 23 palabras y el límite inferior combinando argumentos de conteo de fibras con instancias de CNF refutadas por LRAT para demostrar que no puede existir una cobertura de 22 palabras.

Autores originales: Andreas Florath

Publicado 2026-06-16

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Andreas Florath

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás intentando empaquetar un conjunto de "redes de seguridad" especiales en una habitación gigante de cuatro dimensiones llena de millones de puntos. El objetivo es asegurar que cada uno de los puntos en la habitación esté a una distancia corta (digamos, dos pasos) de al menos una red de seguridad.

La pregunta que los matemáticos se han estado haciendo es: ¿Cuál es el número mínimo absoluto de redes de seguridad que necesitas para cubrir toda la habitación?

Para un tipo específico de habitación (donde cada dimensión tiene 8 valores posibles), la respuesta se ha reducido a un rango minúsculo: es o bien 22 redes o 23 redes. Este artículo, escrito por Andreas Florath, demuestra definitivamente que 23 es el número mágico. No puedes hacerlo con 22.

Aquí te explicamos cómo funciona la demostración, desglosada en analogías sencillas:

1. La demostración de dos partes

Para demostrar que la respuesta es exactamente 23, el autor tuvo que hacer dos cosas, como demostrar que una puerta está cerrada por ambos lados:

El Límite Superior (Mostrar que 23 funciona): El autor simplemente encontró una lista específica de 23 redes de seguridad y la comprobó contra cada punto de la habitación. Es como decir: "Aquí hay un mapa de 23 estaciones de bomberos; he recorrido cada calle y confirmado que ninguna casa está a más de dos manzanas de una estación". Esta parte es fácil de verificar porque el autor simplemente mostró la lista.
El Límite Inferior (Mostrar que 22 falla): Esta es la parte difícil. El autor tuvo que demostrar que es imposible cubrir la habitación con solo 22 redes. No puedes simplemente comprobar todas las disposiciones posibles de 22 redes porque hay demasiadas (más que los átomos en el universo). En su lugar, el autor utilizó un truco lógico ingenioso para demostrar que cualquier intento de usar 22 redes dejaría inevitablemente un hueco.

2. El trabajo de detective del "Par Faltante"

Para demostrar que 22 redes no son suficientes, el autor no miró las redes directamente. En su lugar, miró lo que faltaba.

Imagina que la habitación es una cuadrícula gigante. Si eliges cualquier par de coordenadas (como "suelo" y "pared"), puedes observar todos los pares de valores que aparecen en las redes.

La Lógica: Si un par de valores específico (por ejemplo, "Suelo 3, Pared 5") nunca aparece junto en ninguna de tus 22 redes, eso es un "par faltante".
El Gráfico: El autor dibujó un mapa (un grafo) para cada par de coordenadas, marcando las combinaciones "faltantes".
La Contradicción: La demostración muestra que si solo tienes 22 redes, las reglas de la geometría obligan a que estos mapas de "pares faltantes" formen una forma específica y prohibida, un "clique" (un nudo apretado de conexiones faltantes). Pero si esa forma existe, significa que hay un punto en la habitación que está demasiado lejos de cualquiera de tus redes. Por lo tanto, 22 redes no pueden cubrir la habitación.

3. El rompecabezas de los "Bloques"

Cuando el autor analizó el caso en el que alguien intenta usar exactamente 22 redes, descubrió que las redes tendrían que organizarse en una estructura muy rígida, similar a bloques (específicamente un patrón de 3 + 3 + 2).

Piensa en esto como intentar construir un muro con 22 ladrillos. Las matemáticas muestran que, para evitar huecos, los ladrillos tendrían que apilarse en tres grupos específicos. Sin embargo, cuando intentas construir la sección final del muro utilizando los ladrillos restantes, la geometría se rompe. Es como intentar encajar un clavija cuadrada en un agujero redondo; la estructura requerida para cubrir la habitación simplemente no puede existir con solo 22 piezas.

4. La comprobación "Lean" de la computadora

Aquí es donde el artículo se vuelve de alta tecnología. Debido a que la lógica del "par faltante" implica revisar miles de pequeñas posibilidades (como un puzzle de Sudoku con millones de celdas), el autor utilizó un programa informático llamado Lean.

El SAT Solver: El autor utilizó un potente programa informático (un SAT solver) para comprobar la enorme lista de posibilidades y decir: "Esta disposición específica es imposible".
El Certificado: Normalmente, tenemos que confiar en la computadora. Pero aquí, la computadora no solo dijo "Imposible". Produjo un certificado (un recibo paso a paso de su lógica).
La Verificación: El programa Lean leyó luego ese recibo y verificó cada uno de los pasos de la lógica de la computadora por sí mismo. Esto significa que la prueba está verificada por máquina. No tenemos que confiar en el cerebro de la computadora; solo tenemos que confiar en la capacidad de Lean para leer el recibo, que es mucho más pequeño y fácil de verificar.

Resumen

El artículo demuestra que para esta habitación específica de cuatro dimensiones con 8 opciones por dimensión:

23 redes son suficientes (aquí está la lista).
22 redes no son suficientes (aquí hay una prueba lógica de que cualquier intento de usar 22 redes crea un vacío inevitable).

El resultado es una prueba "Certificada por Lean", lo que significa que todo el argumento —desde la gran lógica hasta las diminutas comprobaciones informáticas— ha sido verificado por un sistema de software matemático formal, sin dejar lugar al error humano o a la duda. La respuesta es exactamente 23.

Resumen Técnico: Una prueba de $K_8(4,2) = 23$ certificada por Lean

Planteamiento del problema
El artículo aborda la determinación del número de cobertura exacto $K_q(n,r)$ , definido como el tamaño mínimo de un código de cobertura de radio- $r$ en el espacio de Hamming $q$ -ario de longitud $n$ . Específicamente, resuelve el valor para el caso octonario con longitud 4 y radio 2: $K_8(4,2)$ . Antes de este trabajo, los intervalos existentes (las tablas de Kéri) situaban este valor en el intervalo $[22, 23]$ . El límite inferior fue derivado del límite de dominio de la torre de Rodemich, mientras que el límite superior fue sustentado por límites de alfabeto grande. El objetivo era cerrar este intervalo probando el límite inferior $K_8(4,2) \ge 23$ .

Metodología
La prueba se formaliza en el demostrador de teoremas Lean 4 utilizando la biblioteca mathlib. Emplea un enfoque de "prueba portadora" donde el resultado se establece mediante dos certificados independientes: un límite superior explícito y un límite inferior estructural.

Límite Superior ( $K_8(4,2) \le 23$ ):
Los autores proporcionan un código explícito que consta de 23 palabras de código en $(\text{Fin } 8)^4$ . La prueba formal verifica dos condiciones: que la cardinalidad del conjunto es a lo sumo 23, y que cada palabra en el espacio ambiente (4096 palabras) está a una distancia de Hamming de a lo sumo 2 de al menos una palabra de código. Esta es una verificación finita exhaustiva.
Límite Inferior ( $K_8(4,2) \ge 23$ ):
El núcleo del artículo es un argumento de no existencia estructural para cualquier hipotética cobertura $C^*$ con $|C^*| \le 22$ . La prueba procede mediante una secuencia de reducciones:
- Conteo de fibras: Para una cobertura hipotética, los autores definen "fibras" $C^*_{i,a}$ (palabras de código con el símbolo $a$ en la coordenada $i$ ). Demuestran que cada fibra debe contener al menos dos palabras de código. Esto establece una base de 16 palabras de código ( $8 \text{ símbolos} \times 2$ ) por coordenada, dejando un "presupuesto" de a lo sumo 6 palabras de código excedentes para el caso $|C^*|=22$ (o 5 para $|C^*| \le 21$ ).
- Grafos de pares faltantes: La prueba cambia a un punto de vista "inverso", analizando qué pares de símbolos están faltantes en las proyecciones del código sobre los pares de coordenadas. Estos pares faltantes forman grafos $E_{ij}$ .
- Caso $|C^*| \le 21$ : Utilizando el pequeño presupuesto de exceso, los autores demuestran mediante conteo combinatorio que los grafos de pares faltantes deben contener un "clique cuatripartito simultáneo" (un conjunto de cuatro símbolos $a,b,c,d$ tales que los seis pares de coordenadas están ausentes). El Lema 7 demuestra que tal clique no puede existir en una cobertura válida de radio-2, lo que descarta coberturas de tamaño 21 o inferior.
- Caso $|C^*| = 22$ : Para el caso restante, la prueba reduce el problema a una clasificación finita del "perfil" de los grafos de pares faltantes. Los autores muestran que cualquier perfil válido debe exhibir una estructura específica de "bloque común $3+3+2$ ".
- Integración SAT/LRAT: La clasificación de estos perfiles es demasiado grande para la enumeración manual. Los autores codifican las restricciones (límites de grado de fila/columna y la condición de no-clique) en instancias de Forma Normal Conjuntiva (CNF). Utilizan un resolvedor SAT no confiable para generar refutaciones de RAT Lineal (LRAT) (pruebas de insatisfacibilidad).
- Verificación Formal: Lean analiza estos certificados LRAT y reproduce mecánicamente las refutaciones para probar que no existe un perfil válido para una cobertura de 22 palabras.
- Contradicción Final: Incluso si se asumiera una estructura de bloque común, los autores derivan una contradicción en el "componente de 2 símbolos" de la estructura. Este componente requeriría un arreglo binario de fuerza-2 de longitud 4 con a lo sumo 4 filas, lo cual es matemáticamente imposible.

Contribuciones Clave

Valor Exacto: El artículo establece el valor exacto $K_8(4,2) = 23$ , cerrando el intervalo previamente conocido $[22, 23]$ .
Límite Inferior Formalizado: Proporciona una prueba totalmente formalizada en Lean 4 que excluye todas las coberturas de 22 palabras. Esto se logra no mediante argumentos de volumen, sino mediante obstrucciones estructurales derivadas de los conteos de fibras y los grafos de pares faltantes.
Artefacto de Prueba Portadora: El resultado se empaqueta como un artefacto de Lean que contiene el código explícito, los lemas estructurales, las instancias CNF y las refutaciones LRAT. Crucialmente, el resolvedor SAT no es parte de la base de computación confiable; Lean verifica los certificados LRAT internamente.
Patrón para Límites Inferiores Computacionales: El artículo introduce un patrón reutilizable para adjuntar evidencia producida por resolvedores a los límites inferiores de códigos de cobertura. Separa el "descubrimiento" (resolvedor no confiable) de la "verificación" (núcleo de Lean confiable), permitiendo que los grandes problemas de clasificación finita se resuelvan computacionalmente manteniendo la corrección formal.

Resultos
El resultado principal es el teorema $K_8(4,2) = 23$ .

Límite Superior: Probado mediante un código explícito de 23 palabras.
Límite Inferior: Probado mostrando que una cobertura de tamaño 22 conduce a una contradicción mediante un "sistema de bloques comunes $3+3+2$ " forzado que implica la existencia de un arreglo binario imposible.
Rendimiento: La verificación formal involucra recursos computacionales significativos. La reproducción en modo kernel del archivo de prueba principal requirió aproximadamente 143 GiB de RAM, mientras que el modo nativo redujo esto a unos 5.5 GiB. La fase de verificación de LRAT tomó aproximadamente 17 minutos en modo kernel.

Significancia y Reivindicaciones
El artículo reclama su significancia principalmente en el ámbito de la matemática formalizada y la metodología de combinar el razonamiento combinatorio con certificados computacionales.

Cambio Metodológico: Demuestra que la combinatoria estructural puede combinarse con evidencia computacional de "prueba portadora". El resolvedor SAT se utiliza para descubrir obstrucciones finitas, pero el puente matemático y la verificación de la salida del resolvedor son manejados enteramente por el demostrador de teoremas.
Frontera de Confianza: El trabajo clarifica la frontera de confianza en las pruebas formales que involucran resolvedores SAT. El resolvedor es no confiable; el núcleo de Lean verifica los certificados LRAT y la deducción lógica que conecta estos certificados con la declaración del código de cobertura.
Escalabilidad: El resultado sirve como un caso de prueba para manejar problemas de códigos de cobertura que son demasiado grandes para una prueba manual pero lo suficientemente pequeños como para ser reducidos a problemas de clasificación finita resolubles mediante resolvedores SAT.
Sin Nuevas Aplicaciones: El artículo no pretende nuevas aplicaciones para el valor $K_8(4,2)=23$ en sí mismo, ni propone nuevos protocolos experimentales. Su contribución es estrictamente la resolución de un problema abierto específico en las tablas de teoría de códigos y la demostración de un flujo de trabajo de verificación formal para tales problemas.