Dan Abramov publica prueba en Lean de la conjetura de Conway

Dan Abramov, el ‘vibe coder’ que llevó el método a las matemáticas

Dan Abramov, creador de Redux y exintegrante del equipo núcleo de React, publicó el 18 de septiembre de 2026 un experimento en su blog overreacted.io titulado «I Vibed a Proof of Conway’s Conjecture». El post documenta un mes de trabajo a tiempo parcial en el que un programador sin formación matemática formal coordinó agentes de IA para producir una demostración en Lean —un lenguaje de demostración asistida por computadora— de un problema abierto planteado por John Conway en 1976.

El título «vibed» es deliberado: recoge la idea del vibe coding que se popularizó a inicios de 2025, según la cual el humano describe la intención a un modelo y delega la ejecución sin verificar cada línea. Abramov llevó el patrón al extremo matemático: dejar que los agentes hicieran investigación mientras él orquestaba.

La prueba aún no fue verificada de forma independiente por matemáticos humanos, aunque sí pasó las verificaciones mecánicas del registro Palomar y, según el autor, algunas personas familiarizadas con Lean y el campo la consideraron plausible. Abramov publica el trabajo e invita explícitamente a que alguien intente refutarlo.

👥 ¿Quieres ir más allá de la noticia?

En nuestra comunidad discutimos las tendencias, compartimos oportunidades y nos ayudamos entre emprendedores. Sin humo, solo acción.

👥 Unirme a la comunidad

¿Qué es la conjetura de refinamiento de Conway?

Los números surreales son una invención —o descubrimiento— de John Conway descrita en su libro de 1976 On Numbers and Games (ONAG), cuyo 50º aniversario es la razón sentimental que empujó a Abramov a atacar el problema. Los números surreales incluyen todos los reales, todos los ordinales y combinaciones intermedias como 75 + ω·3 + 1/ω.

Dentro de ese universo, los enteros omníficos son la «parte entera» del árbol surreal: además de 3 o –5, incluyen a ω, 2ω, ω^ω, –ω/7 y similares.

La conjetura de refinamiento afirma que si tenemos cuatro enteros omníficos a, b, c, d con ab = cd, entonces existen otros cuatro e, f, g, h tales que a = ef, b = gh, c = eg y d = fh. Es el análogo surreal de una propiedad trivial de los enteros usuales: si 210 = 10 × 21, podemos descomponer 10 como 2 × 5 y 21 como 3 × 7, y reagruparlos en 6 × 35. Con ordinales infinitos, esa garantía no es automática, y Conway conjeturó que seguía siendo cierta.

Abramov aclara que esta podría no ser la última conjetura pendiente de Conway sobre sus números, pero el aniversario del libro lo convenció. La elección vino además sugerida por Claude, al que le pidió que eligiera un problema abierto del campo «que tirara de él».

El laboratorio multi-agente: PM, Math, Red, Random, Lean y Cafetería

El núcleo del post es la metodología. Tras varios intentos fallidos con sesiones únicas que producían «ensalada de palabras» matemática, Abramov aterrizó en una arquitectura con varios agentes ejecutándose en paralelo usando Codex (el agente local de OpenAI) y, cuando se quedaba sin tokens, Claude:

PM: dirige hacia el objetivo y consolida trabajo.
Math (varios): buscan los siguientes «breakthroughs».
Red: intenta romper lo que proponen los Math.
Random: anima a explorar lo que quiera.
Lean: formaliza el trabajo matemático aceptado.
Cafetería: retransmite cada mensaje a todos los demás agentes, emulando un chat grupal.

Codex ofrecía dos funciones clave que Abramov destaca: un sistema de Goals que recordaba periódicamente a cada sesión su rol, y la posibilidad de que las sesiones se enviaran mensajes entre sí. Eso le permitió al PM coordinar tareas sin que él estuviera pegado a la pantalla.

Un giro que funcionó: invertir los roles del agente Red y Random. El Red, entrenado para destruir, recibió de pronto la instrucción de ser creativo; publicó una construcción en la cafetería, y el Random la retomó. Esa idea, según Abramov, terminó conectando los puntos de la prueba final —aunque después se «quemó en un fuego» y hubo que redescubrirla más adelante.

El problema del ‘word salad’ y por qué separar el código verificado del experimental importó

La mayor parte del post es una confesión de los fracasos intermedios. Los primeros intentos —un único prompt a Claude del tipo «do a breakthrough»— generaron párrafos en lenguaje metálico inventado por el modelo, nombres grandilocuentes para resultados triviales y una inflación retórica que el propio autor compara con «mala ciencia ficción».

Al pasar a ChatGPT (modelo Sol) con la instrucción de criticar lo que Claude había producido, descubrió que efectivamente gran parte era bullshit en un sentido importante: no siempre una ecuación falsa, sino torres de teoremas infladas, etiquetas inventadas e hipótesis condicionales présentées con cadencia de progreso. El propio ChatGPT cuantificó después el resultado: alrededor de un 10–15% del material valía la pena, 35–45% era matemática correcta pero sin contribución, y 40–50% era la categoría peligrosa de «torres infladas».

La solución llegó al separar físicamente el trabajo en dos worktrees de Lean: uno formalizaba matemática peer-reviewed bien establecida, el otro —oculto del primero— intentaba certificar resultados nuevos. La idea era evitar que las abstracciones inmaduras contaminaran las bases aceptadas. Cuando ese segundo Lean pasó la prueba, Abramov lo confirmó con un matemático humano: era un resultado «de nicho pero ahora interesante». Sólo entonces volvió a escalar hacia Conway.

Otro aprendizaje práctico: renombrar el código. Los LLMs heredan terminología inventada de iteraciones previas y la fosilizan dentro de Lean. Abramov pidió a un agente con contexto limpio que renombrara todas las estructuras a letras A, B, C, y a otro, que no había visto los nombres viejos, que eligiera nombres estándar usando un «mapa» del campo generado a partir de los papers de referencia.

¿Qué significa esto para tu startup?

El experimento importa más allá de las matemáticas. Es un caso real de ingeniería de prompts + arquitectura de agentes ejecutada por una sola persona durante semanas para producir un output verificable de forma mecánica. Varias ideas son directamente portables a tu contexto:

La verificación automatizada es el cuello de botella, no la generación. Abramov sólo pudo confiar en su resultado cuando una herramienta externa (Palomar) certificó la prueba. En tu producto, ese es el rol de los tests, de los linters o de un cliente que reporte el bug: sin un mecanismo de «este output pasó una verificación independiente», el agente va a generar textos plausibles pero podridos.
Separar roles reduce la corrupción cruzada. Mantener el agente que verifica el conocimiento aceptado lejos del que explora lo nuevo evitó que contaminaran las bases. En cualquier pipeline de IA que uses, esa separación entre «ground truth» y «exploración» merece ser explícita desde el día uno.
El humano hace de engineering manager, no de autor. Abramov confiesa que no entendía la matemática que estaba aprobando; sólo sabía cuándo los agentes estaban dando vueltas, cayendo en grandilocuencia o certificando resultados propios como correctos. Su trabajo era detectar «deriva» y reiniciar sesiones a tiempo. Es el patrón de delegar la ejecución y conservar la supervisión.

Dos acciones concretas que puedes aplicar esta semana

Monta una «cafetería» en tu flujo de agentes. Si usas varios agentes que persiguen un objetivo común, dales un canal compartido donde cada uno pueda postear hallazgos y leer lo de los demás. Abramov destaca que varios breakthroughs surgieron de combinaciones inesperadas entre agentes que, sin ese canal, habrían trabajado aislados.
Separa físicamente el código «verificado» del «experimental». Dos worktrees, dos bases de datos, dos cuentas: una para conocimiento aceptado por humanos o por herramientas externas, otra para lo que tu IA está generando. Sólo promueve lo experimental a la zona verificada cuando pase un check externo (un test, un linter, un revisor humano). Es la misma lógica que Abramov aplicó para que sus «papers» inventados no envenenaran las matemáticas que ya estaban en Lean.