¿CON QUÉ IA?
A quién le sirve. Investigadores y programadores que mantienen demostraciones formales (en Rocq, Lean o Isabelle) y necesitan repararlas cuando un cambio las rompe, en un caso muy especializado y no de negocio.
Qué hicieron
Codex tenía acceso al repositorio, editó archivos de pruebas en Rocq (un lenguaje para demostrar matemáticamente que un programa es correcto), ejecutó compilaciones concretas y usó un servidor rocq-mcp para ver el estado de cada demostración. Primero arregló las pruebas de VST y luego el teorema de isomorfismo de grafos. Propuso una condición nueva sobre aristas hacia atrás y el autor la revisó. Exigía hablar antes de tocar cualquier definición y rechazó nuevas precondiciones de VST sin pruebas.
Cómo salió
La rama compiló y se integró en el proyecto original como PR 30. El teorema principal se aceptó el 29 de abril y una auditoría posterior eliminó una premisa antigua sobre la ausencia de aristas hacia atrás. Es un solo caso, no un estudio controlado.
Conviene saber
Hace falta supervisión intensa: unas 59 horas de Codex activo, 415 instrucciones humanas y 13.305 llamadas a herramientas en diez días, sin que se midiera ninguna aceleración.
Qué necesitas
- Un proyecto de demostraciones formales que compile, en Rocq (antes llamado Coq), Lean o Isabelle
- Codex u otro agente de programación con acceso a la carpeta del proyecto
- El comando con el que compila tu proyecto, para que el agente pueda lanzarlo
- Git, para ver exactamente qué ha cambiado el agente
- Una persona que conozca el tema y pueda revisar los cambios contra la especificación
Cómo hacerlo tú, paso a paso
- Crea una rama nueva en Git para este trabajo, de modo que el proyecto original no se toque.
- Anota qué se rompió, qué cambio lo causó y qué archivos están afectados.
- Da al agente acceso a la carpeta y dile cómo compilar solo la parte afectada, no todo el proyecto cada vez.
- Si tu asistente de demostraciones tiene un servidor MCP (un conector estándar entre la IA y otras herramientas) que muestre el estado de cada demostración, como rocq-mcp en Rocq, conéctalo para que el agente vea qué falta por probar.
- Pega el prompt de la ficha y fija una regla firme: no cambiar definiciones, especificaciones ni condiciones sin preguntarte antes.
- Arregla por partes: primero las pruebas más locales y después los teoremas grandes. Revisa cada condición nueva que proponga el agente.
- Cuando compile, pide la lista de todo lo modificado y haz que una persona la revise con la especificación en la mano.
En mi proyecto de [Coq, Lean o Isabelle] en [carpeta], la demostración [archivo o lema] se ha roto después de [cambio que hice]. Edita los archivos, ejecuta la compilación y repara la demostración con los cambios locales más pequeños posibles. No debilites ni cambies ninguna especificación ni condición sin preguntarme antes. Habrás terminado cuando compile y me entregues la lista de todo lo que hayas modificado, para que yo la revise.
Consejos
- Que compile no significa que esté bien: una demostración puede compilar porque se haya debilitado lo que afirma. Revisa qué cambió en las definiciones.
- Pide cambios locales y pequeños. Los grandes son mucho más difíciles de revisar.
- Úsalo para el trabajo mecánico y pesado, no para decidir qué debe garantizar la especificación.
Preguntas frecuentes
¿Sirve si no uso Rocq?
El método sí: trabajar en una rama, compilar por partes y prohibir cambios de especificación sin permiso. Las herramientas concretas cambian con Lean o Isabelle.
¿Por qué prohibir que toque las especificaciones?
Porque la forma más fácil de que una demostración compile es hacerla más débil o cambiar lo que afirma. La especificación es lo que quieres garantizar, y solo la debe cambiar una persona.
¿Cuánto cuesta?
El caso no da cifras de coste. Depende de cuánto uses el agente, así que empieza con un teorema pequeño y mide.
Fuentes
En el directorio desde el 3 de octubre de 2026.
aisagroup en Substack
@Ducktumay en X
r/AiForSmallBusiness en Reddit