Personalmente he cruzado una línea, y estoy un poco asombrado. Esta es mi primera prueba completamente automatizada, generada por LLM y auto-formalizada de un nuevo teorema matemático. Déjame plantear el problema: tenemos tres círculos rotatorios con seis posiciones cada uno, todos 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 originalmente noté en un encantador rompecabezas del juego Machinarium de Amanita Design. La tarea no es extremadamente difícil, pero aparentemente tiene dos pruebas: 1. Una búsqueda a fuerza bruta sobre clases de conjugación para representar todas las transposiciones (hice esto hace muchos años pero nunca lo publiqué). 2. Una prueba generada por LLM (en este caso producida hace unos tres meses por GPT-5-Pro), o en realidad dos pruebas, ambas utilizando de manera 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 auto-formalizar esta prueba. Gracias a @HarmonicMath, obtuve acceso a su notable software, Aristóteles. En resumen, esto es lo que hice: A. Generé automáticamente la prueba con un LLM (y la ejecuté varias veces para obtener una versión mucho mejorada). B. Recorté la prueba al texto matemático básico: definiciones, proposiciones, lemas, teoremas, con pruebas suministradas por el LLM. C. Ejecuté el sistema Aristóteles durante la noche (a través de API). Esta mañana recibí una versión completamente formalizada en Lean (unas 700 líneas de código). El código compila, así que ahora tengo un certificado que confirma que la prueba generada por el LLM efectivamente condujo a una solución correcta. Además, obtuve una prueba conceptual, mejor que mi propia fuerza bruta. Estoy planeando llevarlo más allá a una clase más amplia de tales problemas algebraicos. Es un pequeño proyecto, pero para mí personalmente marca un hito. Ahora tengo herramientas que, con mi orquestación, pueden ayudarme genuinamente a descubrir, formalizar y estudiar pruebas de teoremas matemáticos. Esto no es trivial. Preguntas: 1. ¿Cómo escalará esto en el futuro? 2. ¿Cuánto entrenamiento será necesario para tener éxito en tales tareas? 3. ¿Cómo deberíamos tratar la autoría de tales pruebas? 4. ¿Cuál es el papel más profundo de los matemáticos?