Desafio Ramanujan: IA ainda luta para transformar fórmulas matemáticas em provas reais

O Challenge é um projeto de avaliação técnico, não uma ferramenta ou modelo. Criado por Ido Kaminer (Technion) e divulgado por Gil Kalai, ele propõe dez problemas de nível de pesquisa em fórmulas explícitas para constantes matemáticas, como π ou ζ(3), cujas provas completas já são conhecidas pelos organizadores, mas mantidas em sigilo. A meta não é descobrir novas fórmulas, mas exigir que a IA produza derivações simbólicas válidas, com estrutura verificável: provas formais, saídas de CAS (como Mathematica ou SymPy), ou provas humanas com código reprodutível. Isso distingue o Challenge de iniciativas anteriores focadas em geração heurística ou busca numérica.

Ele serve diretamente a pesquisadores que trabalham com raciocínio verificado, agentes matemáticos autônomos e engenharia de provas, não como benchmark genérico, mas como teste de integridade lógica em cadeia: da conjectura à derivação passo a passo, sem saltos não justificados. O fato de exigir reprodutibilidade via código também o alinha com práticas reais de desenvolvimento científico assistido por IA, não só com ambientes formais isolados como Lean ou Coq.

A OpenAI já havia submetido provas ponta a ponta no desafio First Proof em fevereiro [[LINK:/newsletter/ceviu-ia/openai-detalha-suas-primeiras-submissoes-de-provas-matematicas|OpenAI detalha suas primeiras submissões de provas matemáticas]], mas o Challenge é diferente: não testa apenas se a IA 'resolve', mas se ela constrói um caminho lógico que humanos conseguem auditar, entender e reutilizar. Antes, o foco era completude funcional; agora, é transparência estrutural. Também há evolução prática: enquanto o First Proof usava problemas com soluções parcialmente acessíveis, o Challenge mantém todas as provas secretas até o encerramento, forçando a IA a operar sem 'dicas' ocultas ou treino em exemplos similares.

Matemáticos como Terence Tao observam que sistemas atuais geram provas válidas, mas infladas e ininteligíveis, centenas de linhas sem abstração, inúteis para avanço humano. O Challenge pressiona exatamente nisso: provar não é só chegar ao resultado certo, mas explicar *por que* ele segue logicamente. Isso afeta áreas críticas como verificação de software seguro, validação de algoritmos criptográficos e até regulamentação de IA em setores técnicos. Se uma IA não consegue formalizar um teorema simples de forma clara, sua confiabilidade em sistemas de missão crítica fica em xeque, e não há 'ajuste de prompt' que resolva isso.