Eu pessoalmente ultrapassei uma linha, e estou um pouco em admiração. Esta é a minha primeira prova totalmente automatizada, gerada por LLM e auto-formalizada de um novo teorema matemático. Deixe-me apresentar o problema: temos três círculos rotativos com seis posições cada, todos três se intersectando em um total de seis pontos. Prove que o grupo de movimentos que eles geram é o grupo simétrico completo S_{12}. Este é um problema que eu originalmente notei em um lindo quebra-cabeça no jogo Machinarium da Amanita Design. A tarefa não é extremamente difícil, mas aparentemente tem duas provas: 1. Uma busca exaustiva sobre classes de conjugação para representar todas as transposições (eu fiz isso há muitos anos, mas nunca publiquei). 2. Uma prova gerada por LLM (neste caso produzida há cerca de três meses pelo GPT-5-Pro), ou na verdade duas provas, ambas usando de forma brilhante um teorema de Jordan sobre grupos primitivos (ou uma variante intimamente relacionada que é ainda mais direta). ( O que eu estava perdendo até esta noite era uma ferramenta para auto-formalizar esta prova. Graças ao @HarmonicMath, ganhei acesso ao seu notável software, Aristóteles. Em resumo, aqui está o que eu fiz: A. Prova auto-gerada com um LLM (e executei várias vezes para obter uma versão muito melhorada). B. Cortei a prova para o texto matemático essencial—definições, proposições, lemas, teoremas—com provas fornecidas pelo LLM. C. Executei o sistema Aristóteles durante a noite (via API). Esta manhã recebi uma versão totalmente formalizada em Lean (cerca de 700 linhas de código). O código compila, então agora tenho um certificado confirmando que a prova gerada pelo LLM realmente levou a uma solução correta. Além disso, obtive uma prova conceitual, melhor do que a minha própria busca exaustiva. Estou planejando levar isso adiante para uma classe mais ampla de tais problemas algébricos. É um pequeno projeto, mas para mim pessoalmente marca um marco. Agora tenho ferramentas que, com minha orquestração, podem genuinamente me ajudar a descobrir, formalizar e estudar provas de teoremas matemáticos. Isso não é trivial. Perguntas: 1. Como isso escalará no futuro? 2. Quanto treinamento será necessário para ter sucesso em tais tarefas? 3. Como devemos tratar a autoria de tais provas? 4. Qual é o papel mais profundo dos matemáticos?