A matemática ganhou um colega que não dorme (e que mostra o trabalho)

Na escola, o professor de matemática vivia pedindo para “mostrar a conta”. Pois a IA agora está sendo cobrada do mesmo jeito, e está entregando.

O que rolou

Em 6/10, a OpenAI publicou uma série de resultados matemáticos produzidos por um modelo interno. O detalhe que importa: as provas vieram formalizadas na linguagem Lean, um sistema em que o computador confere cada passo do raciocínio. Ou seja, ninguém precisa acreditar na palavra do modelo, porque a verificação é automática.

Nove dias depois, em 15/10, a Simons Foundation anunciou um esforço de US$ 15 milhões, somando a fundação, a Anthropic e a OpenAI, para ajudar os matemáticos a avaliar e usar o que a IA começa a produzir. A parte da OpenAI é de US$ 5 milhões.

A virada

Quem banca a ajuda aos matemáticos para lidar com a IA inclui as próprias empresas de IA. Dá para ler isso de dois jeitos: responsabilidade (elas criaram o problema e ajudam a resolver) ou estratégia (quem financia a régua ajuda a definir a régua). As duas leituras cabem.

E aí?

O modelo de trabalho que aparece aqui serve para muita área além da matemática: a IA propõe, uma verificação independente confere e a pessoa decide o que vale a pena perguntar. No seu trabalho, a pergunta é qual é o “Lean” que confere o que a IA te entrega.

Resumo original do Rolou na IA a partir das fontes primárias (OpenAI e Simons Foundation).