A lição amarga na prova automática de teoremas: modelos base atropelam soluções específicas

O texto é um relato em primeira pessoa de alguém que montou, em alguns fins de semana, um provador automático de teoremas inteiramente em Lean. O autor criou um fork privado do Lean4 (o open-source estável, diz ele, serve para formalizar teoremas existentes, mas não para busca de provas com alta eficiência). Também escreveu um harness próprio, porque os harnesses padrão do Claude Code e do Codex se perdiam no contexto longo e ficavam caros. Ele distribuía computação, controlava limites de API e fazia cache de lemas internos.

Com o GPT-5.5, o sistema provou alguns teoremas novos, mas devagar, com muitas afirmações incorretas. Com o GPT-5.6 Sol, a eficácia melhorou. O autor gerou algumas centenas de milhares de linhas de Lean tentando o problema do grafo de Moore de grau 57 e a conjectura de Hadwiger, sem fechar a prova. Com o GPT-6 Astra, o salto foi maior, sobretudo na intuição do modelo base para estratégias de prova. Quatro semanas depois, segundo ele, a OpenAI rodou um modelo ainda não lançado em 4.000 problemas, com cerca de 3,5 horas de computação equivalente ao ChatGPT Pro Thinking por problema, o que ele estima em no máximo uns 100 dólares por problema. O resultado incluiu uma refutação de Hadwiger. O próprio autor admite que não mediu nada com evals: suas conclusões são impressões, já que benchmarks públicos como o Frontiermath são contaminados e ele não criou evals privados.

A cobertura anterior ajuda a situar a trajetória. Em 23 de fevereiro de 2026, o CEVIU noticiou "OpenAI Detalha Suas Primeiras Submissões de Provas Matemáticas", sobre tentativas de prova de ponta a ponta nos dez problemas do First Proof. Em 3 de agosto de 2026, veio "Revolução na Matemática: IA da OpenAI Soluciona Problemas em Aberto", sobre um modelo não lançado que resolveu dez problemas em aberto. O relato do autor é a leitura de quem tentava o mesmo caminho com engenharia própria e foi ultrapassado por esse tipo de resultado. Em 9 de setembro de 2026, o CEVIU também publicou "A 'Mineração' de Problemas na Matemática Atinge Ponto Crítico", que trata do esgotamento de problemas relevantes, tema vizinho da preocupação do autor com o fim da legibilidade das melhorias.

Para quem constrói agentes e harnesses sobre modelos de linguagem, a leitura é incômoda: parte do investimento em orquestração específica pode ser engolida pela próxima versão do modelo base. É uma opinião do autor, apoiada em experiência pessoal e sem evals, não um resultado medido. Ainda assim, vale tratar camadas de engenharia como descartáveis e priorizar o que não depende da fraqueza atual do modelo.