1
trsthales
3 min de leitura ·

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?

Carregando publicação patrocinada...
2

Métodos formais nunca falharam por ser ideia ruim. todo mundo sabia que era o santo graal, só que a chave custava 69 doutores-mês para cada 4200 linhas de código. Agora o custo despencou pra zero, e quando o custo de uma obviedade tende a zero não tem debate, tem inevitabildiade.

Daqui a pouco tem estagiário empurrando prova de refinamento pra produção sem saber o que é uma tripla de hoare do mesmo jeito que hoje empurra container sem saber o que é cgroup, e por isso vai funcionar.

Mas o futuro não é simplesmente “o modelo escreveu uma prova em Lean, compilou, acabou”. Isso prova que a prova está correta. Não prova que formalizou o problema certo. Se o requisito tá torto você ganha um certificado de excelência matemática pra sua cagada. Parabéns.

O futuro é o famigerado spec-driven development levado às últimas consequências.

Você escreve uma intenção ambígua, porque aparentemente foi para isso que a civilização inventou a escrita. Um agente transforma aquilo em linguagem natural controlada. Outro extrai uma especificação formal, gera contratos, invariantes e propriedades temporais. Outro refina isso em máquinas de estado e arquitetura. Outro finalmente gera código. E se você for insano o suficiente, o último faz logo o RTL, por até a CPU vai ser coisa obsoleta em breve. Em cada passagem, o nível inferior vem acompanhado da prova matemática que refina o superior corretamente. E aí podemos finalmente dizer a frase proibida:

Você não precisa revisar o código gerado.

E quando uma prova falha, o erro não vai morrer lá embaixo como 14 páginas de símbolos incompreensíveis produzidas pelo Lean ou pelo SMT solver. Ele sobe como calor. Cada nível preserva origem, contexto e justificativa atravessando toda a compilação. Até que o absurdo técnico encontrado a cinco níveis de profundidade reapareça para o humano como um diagnóstico mundano:

requirements/braking.md:47: a expressão “o sistema deve responder rapidamente” não define um limite de tempo suficiente para provar a propriedade de segurança.

Você corrige uma frase mal escrita no Markdown e manda compilar o sistema inteiro outra vez. E é por isso que a profissão não acaba. Alguém ainda tem que dizer o que caralhos quer. Era isso o trabalho o tempo inteiro, você só não tinha percebido por que estva ocupado escrevnedo código.

No fim, o código-fonte vira apenas mais um IR. Um artefato intermediário feio, enorme e descartável que nenhum ser humano deveria perder tempo lendo ou escrevendo, exatamente da mesma forma que aconteceu com o assembly. Não porque a IA ficou confiável. Porque finalmente construímos um pipeline baseada na premissa correta de que ela não merece confiança.

E eu realmente não sei por que ainda não existem dez mil skills fazendo isso. A teoria está escrita há décadas. Os velhos sábios deixaram tudo documentado enquanto o restante da indústria discutia se precisava mesmo escrever requisito antes da sprint.

Então vá ler Rigorous Software Development e Formal Methods for Software Engineering, transforme 60 anos de ciência da computação ignorada numa esteira de agentes e lance isso como “Formal Vibes” numa landing page com gradiente roxo e fique bilionário. Esquece o Lean. Lean é bonito, tem hype, mas quem tem compilador verificado de ponta a ponta é o Coq.

Enquanto qualquer wrapper de API com quatro prompts e um README.md escrito pelo ChatGPT explode no GitHub, CertiRocq e CompCert continuam lá, pegando poeira, contendo algumas das peças mais valiosas já produzidas pela ciência da computação. Então aponta seu agente para aqueles repositórios, manda ele construir o front-end de Markdown para Gallina, chama o resultado de Rocqstar e colete seu cheque.

1