Every Nonnegative Integer Is a Sum of a Triangular, a Pentagonal, and a Heptagonal Number

Resumen Técnico: Todo Número Entero No Negativo es la Suma de un Número Triangular, un Pentagonal y un Heptagonal

Planteamiento del Problema
El artículo aborda una conjetura registrada como OEIS A287616, propuesta originalmente por Zhi-Wei Sun. La conjetura postula que todo entero no negativo $n$ puede representarse como la suma de un número triangular, un segundo número pentagonal y un segundo número heptagonal. Formalmente, para cada $n \in \mathbb{N}$, existen $x, y, z \in \mathbb{N}$ tales que:
$$n = \frac{x(x+1)}{2} + \frac{y(3y+1)}{2} + \frac{z(5z+1)}{2}$$
Los autores distinguen esto de los problemas de números poligonales "generalizados" donde las variables pueden variar sobre todos los enteros; aquí, las variables son estrictamente no negativas.

Metodología y Estrategia de Demostración
La demostración procede transformando el problema aditivo en un problema de representación restringida para una forma cuadrática ternaria diagonal.

1. Reducción al Cuadrado:
   Utilizando identidades elementales ($8T(x)+1=(2x+1)^2$, etc.), el problema se reduce a representar enteros de la forma $m = 120n + 23$ mediante la forma cuadrática:
   $$Q(u, v, w) = 15u^2 + 5v^2 + 3w^2$$
   El objetivo es encontrar una representación donde $u$ sea positivo e impar, $v \equiv 1 \pmod 6$, y $w \equiv 1 \pmod{10}$.

2. La Semilla Primitiva (Existencia):
   La demostración establece primero que todo $m \equiv 23 \pmod{120}$ admite una representación integral primitiva por $Q$ (donde $\gcd(u,v,w)=1$).

   • Principio Local-Global: Los autores utilizan el teorema de Hasse–Minkowski y la estructura específica del género de $Q$. El género de $Q$ consiste exactamente en dos clases: la clase de la propia forma $Q$ y la clase de una forma "compañera" $g_2(x,y,z) = 2x^2 - 2xy + 8y^2 + 15z^2$.
   • Transferencia: Si $m$ es representado por la compañera $g_2$, una serie de transformaciones explícitas (que involucran involuciones e isometrías racionales) transfiere esta representación a $Q$, preservando la primitividad. Este paso se basa en resultados clásicos de la teoría de números (Hasse–Minkowski, teoría de géneros) que se citan pero no se vuelven a probar dentro de la formalización.

3. Descenso Finito (Convergencia):
   Una vez asegurada una representación primitiva, la demostración emplea un algoritmo de descenso para alcanzar un estado "bueno" (que satisfaga las condiciones de congruencia específicas).

   • Función de Potencial: Se define un potencial lexicográfico $\Phi(u,v,w)$ basado en la paridad y el estado de congruencia de las coordenadas.
   • Cálculo de Movimientos: Tres matrices enteras ($P_{uv}, P_{uw}, P_{vw}$) definen "movimientos" que preservan el valor de $Q$ y la primitividad de la representación, mientras reducen estrictamente $\Phi$.
   • Descensos Elementales: Para la mayoría de los estados, un solo movimiento es suficiente para mejorar el potencial.
   • Cono Residual: Un subconjunto pequeño de estados (el "cono residual") resiste el descenso elemental. Para estos, los autores emplean un argumento de determinación de clave finita. Demuestran que el éxito de cualquier secuencia corta de movimientos depende únicamente de un conjunto finito de signos y residuos (una "clave") del vector inicial.
   • Cobertura Asistida por Computadora: El cono residual es cubierto por un conjunto finito de "conos de signo". Para cada cono, un certificado de programación lineal (LP) racional exacto verifica que existe una palabra de escape (una secuencia de movimientos). Esta verificación se realiza utilizando aritmética exacta de enteros y racionales, evitando aproximaciones de punto flotante.

Contribuciones Clave y Resultados

• Demostración de la Conjetura A287616: El artículo proporciona una demostración completa de que la terna $(T, P, H)$ es universal para los enteros no negativos.
• Formalización en Lean 4: Una parte significativa del núcleo matemático (Secciones 2–5 y la lógica de descenso) se ha formalizado en Lean 4 sobre la biblioteca Mathlib.
  • La formalización incluye la reducción al cuadrado, las leyes de transporte, los descensos elementales y el argumento de terminación.
  • La conjetura misma está verificada por máquina.
  • Las únicas excepciones a la formalización completa son:
    1. El principio local-global clásico del género (Hasse–Minkowski + el hecho de las dos clases del género), que se cita como un axioma.
    2. La cobertura finita del cono residual, que se trata como un input verificado por computadora (un axioma derivado de certificados exactos).
  • El equipo de agentes "MechMath Agent Team" generó tanto la demostración en lenguaje natural como la formalización en Lean.

Significancia y Reivindicaciones
El artículo afirma resolver la conjetura OEIS A287616 mediante una combinación de teoría de números clásica y verificación exacta asistida por computadora. Su significancia radica en:

1. Verificación Rigurosa: Al formalizar la demostración en Lean, los autores aseguran que la estructura lógica, la mecánica de descenso y las transformaciones de equivalencia estén libres de error humano.
2. Método de Demostración Híbrido: El trabajo ejemplifica un enfoque "híbrido" donde la teoría profunda (teoría de géneros) se combina con una verificación exhaustiva y exacta por computadora (coberturas de programación lineal) para resolver un problema que es inabordable mediante métodos puramente manuales o puramente heurísticos.
3. Transparencia de Dependencias: La formalización aísla explícitamente los inputs no formalizados (los teoremas clásicos citados y los certificados computacionales), haciendo que la estructura de dependencia de la demostración sea auditable. Los autores enfatizan que el "núcleo matemático" está completamente formalizado, mientras que el "input computacional" se reduce a un certificado finito y exacto.

El artículo no propone nuevas aplicaciones o direcciones experimentales futuras, sino que se centra estrictamente en la resolución de la conjetura de teoría de números específica y en la demostración del flujo de trabajo de formalización.