correcto. sí, soy escéptico de que los LLMs creen nuevas matemáticas perspicaces porque eso requiere un pensamiento fuera de lo común, en lo que son malos. pero los LLMs pueden resolver problemas matemáticos muy difíciles (eso es diferente), lo cual es realmente genial, siempre que no requieran "nuevas definiciones perspicaces". algunos problemas matemáticos requieren "nuevas definiciones perspicaces", y son difíciles precisamente por eso. nunca es que sean inherentemente "pesados" en algún sentido computacional, sino que requieren "imaginación" y "creatividad" para conceptualizar estructuras maravillosas que nadie ha examinado antes. por ejemplo, la prueba del Último Teorema de Fermat requirió el desarrollo de maquinaria matemática completamente nueva: curvas elípticas, formas modulares y la conjetura de Taniyama-Shimura; conceptos que no existían cuando se planteó el problema por primera vez. así que, si tuviéramos LLMs en 1650, no importa cuánto intentaran resolver el FLT - incluso si les dejabas calcular durante siglos - nunca podrían hacerlo, porque estarían pensando dentro de los límites de las estructuras matemáticas que existían en ese entonces, y literalmente no hay un camino hacia una solución. ahora, el día que los LLMs comiencen a inventar estructuras matemáticas genuinamente nuevas, ese será el momento en que podrán probar teoremas "difíciles". esa es la única y única cosa que los separa de poder hacerlo. ahora, esto expone la pregunta más difícil: ¿qué es incluso un "nuevo concepto matemático perspicaz"? muchas cosas cuentan como un "nuevo concepto". Puedo escribir fácilmente algunas palabras aleatorias en Lean, y habré creado un concepto matemático completamente nuevo que nadie ha hecho antes. y los LLMs pueden hacer eso también. eso es lo suficientemente fácil. la parte "perspicaz" es lo que importa aquí. ¿qué hace que algo sea "perspicaz" o "interesante"? ¿por qué los números complejos son más interesantes que definiciones aleatorias? ¿cómo medimos objetivamente cuán perspicaz es una definición en Lean?