Codex Swarm afirma 19 soluciones a problemas de Erdős

Un proyecto matemático destacado en Hacker News dice que usó 20 cuentas de Codex funcionando en paralelo para abordar problemas abiertos de erdosproblems.com — y ahora lista 19 soluciones propuestas, incluidas 13 soluciones completas formalizadas en Lean 4.

El sitio, Starfleet Math, se cuida de señalar que muchos problemas marcados como «abiertos» pueden ya tener respuestas informales o parciales en línea, y dice que intentó evitar esos casos pero «probablemente falló en ciertos casos». También pide a los lectores que informen errores de atribución.

Dos ejemplos destacan en el material proporcionado.

Para el problema #123 de Erdős, que tiene un premio de $250, el proyecto afirma una prueba completa de la versión no degenerada prevista: para enteros a, b, c > 1, coprimos por pares, todo entero suficientemente grande puede escribirse como suma de términos distintos de la forma a^i b^j c^k, sin que ninguno de los términos elegidos divida a otro. El informe dice que el principal obstáculo fue construir un intervalo semilla multiplicativamente amplio, y que el paso clave fue una «cáscara interior opcional» en un único nivel de exponentes homogéneos. El teorema final está formalizado en Lean como Erdos123.erdos_123, y el proyecto afirma que la compilación no contiene marcadores de posición de prueba ni sorryAx. También señala que la fórmula literal de la página web a, b, c ≥ 1 es falsa en (1,1,1), por lo que el resultado formal usa a, b, c > 1.

Recomendado

Módulo solar del 31% sustituye el indio por barato óxido de estaño

Para el problema #254 de Erdős, el proyecto afirma haber probado que si A ⊆ ℕ satisface tanto una condición de crecimiento de cáscaras diádicas como ∑_{n∈A} ‖θn‖ = ∞ para todo real 0 < θ < 1, entonces todo número natural suficientemente grande es suma de elementos distintos de A. El teorema aparece en Lean como Erdos254.erdos_254. Según el informe, las dos jugadas clave de la prueba fueron demostrar que el conjunto de fases «malas» es numerable y luego reemplazar la maquinaria ergódica faltante por una prueba espectral finito-cíclica.

La página presenta cada resultado con un enunciado del problema, un teorema reclamado, un informe detallado y un enlace de descarga etiquetado «Solución completa y verifica con tu IA». El número del titular sigue siendo el remate: 19 soluciones propuestas, 13 soluciones completas, todas obtenidas con una ejecución paralelizada de 20 cuentas de Codex.