Enquanto discutíamos se a IA ia substituir devs, ela começou a quebrar problemas matemáticos de 80 anos: o que está acontecendo?

Fala pessoal!

Passamos os últimos dois anos debatendo se a IA ia acabar com as vagas de júnior, se vibe coding era o futuro ou se engenharia de prompt era profissão. Mas enquanto o mundo de desenvolvimento discutia CRUD e autocompletion, um terremoto silencioso aconteceu em outro departamento: na matemática pura e na ciência da computação teórica.

Nas últimas semanas, modelos de IA começaram a derrubar conjecturas matemáticas abertas que estavam sem solução há 30, 80 e até mais de 100 anos.

O que chama a atenção não é o "hype", mas a mecânica de engenharia por trás desses avanços. Vale a pena analisar os 4 pontos do que realmente está acontecendo:

• O segredo não é o modelo sozinho, é o compilador (Lean):
  Diferente de código em Python ou JavaScript onde a IA alucina e passa despercebido, a matemática formal possui "compiladores" de prova (como o Lean 4). Quando a OpenAI ou a Anthropic colocam um modelo para resolver um problema, a IA gera a prova em linguagem formal e o compilador do Lean valida matematicamente se a prova é 100% rigorosa. Se houver um erro de lógica, o compilador rejeita na hora. Isso elimina o problema da alucinação na raiz através de um loop fechado determinístico.

• A força bruta de subagentes (O caso do criador do Bun):
  O Jarred Sumner (criador do Bun) colocou o Claude Code para trabalhar em uma das perguntas mais famosas da matemática: a Hipótese de Riemann. O setup não foi um simples chat: foram 60 subagentes trabalhando em paralelo, executando 2.400 comandos de shell, centenas de scripts Python auxiliares e consumindo mais de 31 milhões de tokens de saída para elevar o limite inferior dos zeros na linha crítica de 41,6% para 67,2% — com a prova formal gerada e validada no Lean.

• Quebra de conjecturas clássicas por contraexemplos minúsculos:
  A Conjectura de Dinitz-Garg-Goemans (um problema clássico de teoria dos grafos e roteamento aberto há 30 anos) foi derrubada quando o modelo encontrou um contraexemplo elegante: uma rede minúscula de apenas 7 nós e 9 arestas onde o fluxo fracionário era mais barato do que o fluxo único.

A Conjectura Jacobiana (problema de geometria algébrica em aberto desde 1939, listado entre os mais difíceis do século 21) teve um contraexemplo gerado por IA com assistência humana.

Vários problemas da lista lendária de Paul Erdős foram resolvidos em questão de dias.
A reação dos matemáticos de elite (Terence Tao):
O impacto foi tão grande que matemáticos do calibre de Terence Tao (medalha Fields) alertaram no Congresso Internacional de Matemáticos sobre uma "crise nos fundamentos das práticas e valores matemáticos". Pesquisadores de 15 universidades chegaram a publicar a Declaração de Leiden pedindo diretrizes sobre o uso de IA na pesquisa matemática.

## O que isso ensina para quem desenvolve software?
A grande lição desse movimento não é que "a IA virou um gênio mágica", mas sim o poder da arquitetura híbrida:

• Um modelo de linguagem sozinho é probabilístico e falho.
• Um modelo de linguagem acoplado a um verificador determinístico (um compilador, uma suíte de testes de mutação ou um assistente de prova como o Lean) vira um motor de busca combinatória quase imbatível.

A fronteira real do desenvolvimento com IA não está em ficar gerando código solto na tela, mas em construir esteiras com ambientes de verificação formal onde a máquina pode explorar milhões de caminhos e o compilador/teste garante os invariantes.

Vocês têm acompanhado essa transição da IA para provas formais e compiladores? Acham que linguagens com verificação formal rígida (tipo Lean, Rust ou TLA+) vão se tornar o padrão para trabalhar com agentes autônomos?