análise correta. sim, sou cético de que os LLMs criarão novas e perspicazes matemáticas porque isso requer pensamento fora da caixa, no qual eles são fracos. mas os LLMs podem resolver problemas matemáticos muito difíceis (isso é diferente), o que é realmente legal - desde que não exijam "novas e perspicazes definições". alguns problemas matemáticos exigem "novas e perspicazes definições", e eles são difíceis especificamente por causa disso. nunca é que eles sejam inerentemente "pesados" em algum sentido computacional, mas que requerem "imaginação" e "criatividade" para conceitualizar estruturas maravilhosas que ninguém olhou antes. por exemplo, a prova do Último Teorema de Fermat exigiu o desenvolvimento de uma maquinaria matemática completamente nova - curvas elípticas, formas modulares e a conjectura de Taniyama-Shimura - conceitos que não existiam quando o problema foi proposto pela primeira vez. então, se tivéssemos LLMs em 1650, não importa o quão duro eles tentassem resolver o FLT - mesmo que você os deixasse computar por séculos - eles nunca seriam capazes de fazê-lo, porque estariam pensando dentro da caixa das estruturas matemáticas que existiam naquela época, e literalmente não há caminho para uma solução. agora, no dia em que os LLMs começarem a inventar estruturas matemáticas genuinamente novas, é quando eles poderão provar teoremas "difíceis". essa é a única e uma coisa que os separa de serem capazes de fazer isso. agora, isso expõe a pergunta mais difícil: o que é mesmo um "novo conceito matemático perspicaz"? como isso pode ser definido? muitas coisas contam como um "novo conceito". eu posso facilmente escrever algumas palavras aleatórias em Lean, e terei criado um conceito matemático completamente novo que ninguém fez antes. e os LLMs podem fazer isso também. isso é fácil o suficiente. a parte "perspicaz" é o que importa aqui. o que torna algo "perspicaz" ou "interessante"? por que os números complexos são mais interessantes do que definições aleatórias? como medimos objetivamente quão perspicaz é uma definição em Lean?