Una IA contra 353 problemas abiertos de Erdős

Una IA contra 353 problemas abiertos de Erdős#

Un agente de inteligencia artificial que escribe sus pruebas en Lean, un lenguaje donde el compilador revisa cada paso, intentó 353 problemas abiertos de Erdős y resolvió 9. Abrimos las 71 pruebas que publicaron en Zenodo para ver cómo son por dentro, y comparamos lo que lograron otros sistemas con los mismos problemas.

El hallazgo: 9 de 353 problemas de Erdős (2,55 %) y 44 de 492 conjeturas de la OEIS según el paper; las pruebas de Erdős son unas 3,8 veces más largas que las de la OEIS (mediana 764 contra 199 líneas).

Gráfica clave#

¿Cuántos problemas abiertos cerró la IA?

Reproducir#

Abrir en Colab

O localmente:

pip install pandas matplotlib numpy scipy
jupyter execute notebook.ipynb

Datos#

  • datos/pruebas_lean.csv: 71 archivos Lean (69 pruebas completas y 2 parciales) con dominio, líneas de código, lemas auxiliares y respuesta formal

  • datos/tacticas_por_prueba.csv: conteo léxico de 30 tácticas de Lean por archivo (2.130 filas)

  • datos/problemas_intentados.csv: los 353 problemas de Erdős y las 492 conjeturas OEIS intentadas (845 filas)

  • datos/comparacion_sistemas_erdos.csv: problemas de Erdős resueltos por otros sistemas (7 filas, transcrito del material suplementario)

Contenido