Personalmente he cruzado una línea y estoy un poco impresionado. Esta es mi primera demostración totalmente automatizada, generada por LLM y autoformalizada de un nuevo teorema matemático. Déjame plantear el problema: tenemos tres círculos giratorios con seis posiciones cada uno, los tres intersectándose en un total de seis puntos. Demuestra que el grupo de movimientos que generan es el grupo simétrico completo S_{12}. Este es un problema que noté originalmente en un precioso puzle del juego Machinarium de Amanita Design. La tarea no es extremadamente difícil, pero aparentemente tiene dos demostraciones: 1. Una búsqueda por fuerza bruta sobre clases de conjugación para representar todas las transposiciones (lo hice hace muchos años pero nunca lo publiqué). 2. Una demostración generada por LLM (en este caso producida hace unos tres meses por GPT-5-Pro), o en realidad dos demostraciones, ambas usando de forma brillante un teorema de Jordan sobre grupos primitivos (o una variante estrechamente relacionada que es aún más directa). ( Lo que me faltaba hasta esta noche era una herramienta para formalizar esta demostración automáticamente. Gracias a @HarmonicMath, tuve acceso a su extraordinario software, Aristotle. En resumen, esto es lo que hice: R. Generó automáticamente la demostración con un LLM (y la ejecutó varias veces para obtener una versión mucho mejorada). B. Recortó la demostración al texto matemático básico—definiciones, proposiciones, lemas, teoremas—con demostraciones proporcionadas por el LLM. C. Ejecutaba el sistema Aristóteles durante la noche (vía API). Esta mañana recibí una versión totalmente formalizada en Lean (unas 700 líneas de código). El código se compila, así que ahora tengo un certificado que confirma que la demostración generada por el LLM realmente llevó a una solución correcta. Además, obtuve una prueba conceptual, mejor que mi propia fuerza bruta. Estoy planeando llevarlo más allá hacia una clase más amplia de estos problemas de álgebra. Es un proyecto pequeño, pero para mí personalmente marca un hito. Ahora dispongo de herramientas que, con mi orquestación, pueden ayudarme genuinamente a descubrir, formalizar y estudiar demostraciones de teoremas matemáticos. Esto no es trivial. Preguntas: 1. ¿Cómo escalará esto en el futuro? 2. ¿Cuánta formación será necesaria para tener éxito en estas tareas?...