Em julho de 2025 vimos um marco: sistemas desenvolvidos por grandes laboratórios afirmam ter alcançado pontuação equivalente a medalhas de ouro no International Mathematical Olympiad (IMO), incluindo anúncios da DeepMind sobre Gemini e relatórios que colocam modelos da OpenAI em nível semelhante. Mas será que o ChatGPT “ganhou” a Olimpíada como um estudante humano? A resposta exige separar marketing de resultados técnicos: as vitórias recentes são reais em termos de escore, mas surgiram graças a arquiteturas agentivas (pluralidade de submódulos, uso de ferramentas, iterações, debate entre agentes e verificação formal), não por simples “melhorar o LLM”. Em outras palavras, as novas ferramentas representam uma revolução no desenvolvimento da Inteligência Artificial, os agentes de IA. Caso deseje saber mais sobre os agentes de IA e suas aplicações em ambiente empresarial, acesse O que são agentes de IA (Inteligência artificial) ?

A diferença entre LLMs comuns e os modelos que alcançaram a pontuação equivalente a medalha de ouro é impressionante: em uma disputa paralela Gemini 2.5 pro, Grok 4, ChatGPT o3 high, ChatGPT o4-mini high and DeepSeek R1 falharam em produzir uma única solução correta ao serem apresentados aos problemas da referida olimpíada. E, no geral, pela sua própria constituição LLMs tem performance ruim em matemática.

• Em julho de 2025, a DeepMind divulgou que uma versão avançada do seu sistema (Gemini / “Deep Think”) resolveu 5 de 6 problemas da prova do IMO de 2025, alcançando o total de pontos equivalente a uma medalha de ouro.
  
• Relatórios independentes e veículos de imprensa confirmaram que tanto DeepMind quanto OpenAI produziram soluções com qualidade suficiente para serem avaliadas no patamar de “gold-medal level” nas mesmas provas, embora apenas alguns desses sistemas tenham participado oficialmente.
• Esse salto veio depois de uma progressão: em anos anteriores sistemas especializados da DeepMind (ex.: AlphaProof/AlphaGeometry) já haviam atingido níveis próximos a medalha de prata ao automatizar raciocínios geométricos e provas formais.

É crucial distinguir três coisas: 

1. Pontuação (quantos pontos a IA tirou), 
2. Processo (como chegou às soluções) e 
3. Robustez (consistência, capacidade de generalizar). 

Note-se ainda que o nível da olimpíada em questão equivale ao ensino médio, os quais não são o tipo de problema estudado pelos matemáticos profissionais, entre os quais há bastante ceticismo se o desenvolvimento da IA poderá fazê-la alcançar esse nível. 

Modelos de linguagem grandes (LLMs) eram avaliados como “monólitos”: recebem texto e respondem texto.  

A nova geração incorpora agentes, arquiteturas compostas por módulos que planejam, usam ferramentas (solvers simbólicos, buscadores, provadores formais), mantêm memória intermediária e coordenam várias passes de raciocínio. Essa composição permite: 

1. Transformar problema em sub-tarefas 
2. Testar hipóteses programaticamente 
3. Verificar passos com provadores formais ou executores de código 
4. Iterar até consistência. 

Em suma, o salto não é só no LLM, é no ecossistema de agentes que envolvem o LLM. É como se o agente fosse composto por vários indivíduos (LLMs), tivesse posse de calculadora, e possuísse um professor ao seu lado para verificar se a solução proposta é logicamente consistente.

1. Decomposição automática do enunciado em lemas/hipóteses
2. Geração de provas esqueleto em linguagem natural
3. Tradução desses esboços para scripts de verificação (p. ex. sistemas de prova formal) ou código que testa casos
4. Revisões iterativas e “debate” entre sub-agentes para escolher a melhor versão final

Essas etapas aumentam dramaticamente a chance de uma solução correta e verificável, algo que um LLM sozinho raramente atinge de forma confiável em problemas de criatividade matemática profunda.

• Muitos matemáticos apontam que alcançar pontuação não implica criatividade matemática humana: as IAs tendem a combinar técnicas conhecidas e dependem de muito poder computacional e dados anotados; a originalidade e intuição humana ainda são distintas.
• Custo e sustentabilidade: rodar múltiplos agentes, provas formais e iterações consome recursos (tempo de GPU/TPU) — questiona-se a escalabilidade prática fora de grandes laboratórios.
• Robustez e avaliação: provas de IMO são benchmarks úteis, mas não cobrem toda a gama de criatividade ou trabalho matemático em pesquisa.
• Limites teóricos: Problemas em aberto na ciência da computação e na matemática, como P vs NP, podem pôr um limite teórico na capacidade das IAs de resolver certos tipos de problema, mesmo com agentes que desmembram tarefas, executam sub-solvers formais ou usam verificadores, certos problemas matemáticos continuam intratáveis em princípio, não por falta de engenharia, mas por uma barreira de complexidade fundamental

O recente sucesso de ferramentas de IA, apesar dos possíveis limites atuais para a IA, mostram que ferramentas agentivas possibilitam automações de alto valor em tarefas que exigem planejamento + verificação: revisão matemática, auditoria de cálculos, assistência a pesquisadores e geração de código matemático confiável. Para chatbots e automações empresariais, a lição é clara: integrar LLMs a pipelines agentivas (tool calls, verificadores, módulos de memória e controle) aumenta dramaticamente confiabilidade em tarefas complexas, bem além do que “um LLM melhor” sozinho entregaria.