Terry Tao e a matemática assistida por IA e Lean explicada

Em 2014, numa mesa com outros vencedores do Breakthrough Prize em Matemática, Terry Tao fez uma previsão que os colegas acharam mais estranha do que a hipótese de vivermos numa simulação: no futuro, disse ele, artigos matemáticos talvez nem sejam mais escritos em LaTeX, e sim numa linguagem que um software converteria para uma linguagem formal, apontando erro de compilação sempre que um passo da prova não fizer sentido logicamente. Dez anos depois, essa previsão deixou de ser estranha. O Lean é um software que permite escrever provas matemáticas como código, verificado automaticamente por um computador, e Tao se tornou o maior evangelista público do seu uso combinado com inteligência artificial. Se você trabalha com dados, resultados que precisam de verificação ou colaboração em larga escala, o percurso dele importa mesmo fora da matemática pura.

O que aconteceu

Tao é considerado um dos maiores matemáticos vivos: medalha de ouro na Olimpíada Internacional de Matemática aos 12 anos, doutorado em Princeton aos 20, Medalha Fields aos 31. Já colaborava com frequência antes disso, e em 2009 embarcou no Polymath Project, iniciativa do matemático Timothy Gowers para resolver problemas em fóruns públicos abertos a qualquer contribuinte. O modelo funcionou, mas tinha um limite claro: alguém precisava checar manualmente cada contribuição, e esse gargalo de moderação sufocava a própria ideia de colaboração massiva.

Foi só em outubro de 2023 que Tao decidiu aprender Lean, quase dez anos depois de cogitar publicamente esse tipo de verificação automática. A curva de aprendizado o surpreendeu: partes triviais de uma prova em papel, como afirmar que a soma de três números maiores que 1 é pelo menos 3, exigiam garimpar lemas já formalizados numa biblioteca digital chamada Mathlib. Ele levou quase um mês para formalizar uma prova simples de dez páginas.

Menos de um ano depois, Tao liderou a formalização em Lean de um resultado seu com outros três matemáticos de peso (a conjectura polinomial de Freiman-Ruzsa), dividindo a prova em lemas de cinco linhas para que voluntários pudessem contribuir em paralelo. O projeto foi rápido: dentro de um dia já havia um esboço da estrutura, e em poucas semanas dezenas de pessoas, incluindo doutorandas como Yaël Dillies, Paul Lezeau e Aaron Anderson, tinham formalizado pedaços da prova.

Por que isso importa para quem pesquisa com dados

O ponto central da matéria não é sobre matemática pura, é sobre um modelo de trabalho. Tao passou a defender que IA generativa e sistemas de verificação formal deveriam operar juntos: a IA gera hipóteses e explora possibilidades, o sistema formal confirma ou rejeita cada passo. Nenhum dos dois sozinho resolve o problema todo.

Isso se aplica de formas distintas dependendo de onde você está na pesquisa:

1. Se você usa IA para gerar hipóteses ou revisar literatura: o modelo de Tao sugere tratar a saída da IA como ponto de partida, não como resultado final. Ele descreveu as ferramentas de IA em problemas de fronteira como “estudantes de graduação superconfiantes”, que sugerem ideias sem ter o discernimento para separar as boas das ruins quando há pouco dado de treino disponível.
2. Se você trabalha em colaboração com muitos coautores: a lição do Polymath Project é que colaboração aberta aumenta a chance de descoberta por acaso, mas também aumenta a chance de erro. Sem alguma forma de verificação automatizada, a moderação manual vira o gargalo de todo o processo.
3. Se você lida com problemas grandes e difíceis de resolver de uma vez: o método que funcionou tanto no projeto de formalização quanto no Equational Theories foi quebrar o problema em subproblemas pequenos e modulares, resolvíveis em paralelo por muita gente ao mesmo tempo.

O experimento que testou o método na prática

Em setembro de 2024, Tao lançou o projeto Equational Theories: mapear como 4.694 leis algébricas se relacionam entre si, o que gerava 22 milhões de implicações lógicas possíveis para checar. Cada uma precisava ser provada verdadeira ou refutada por contraexemplo.

O grupo testou as leis contra estruturas simplificadas chamadas magmas usando scripts básicos em Python, e resolveu mais de 99% das 22 milhões de implicações em poucos dias. Depois disso, voluntários passaram a usar provadores automáticos de teoremas, sistemas que buscam soluções sozinhos, sem intervenção interativa. Em um mês, restavam 238 casos sem resposta. No fim de março seguinte, apenas quatro implicações continuavam sem solução.

O projeto nunca teve como meta fechar os 22 milhões de casos. Tao queria um mapa completo do território e, no caminho, o grupo topou com uma construção matemática nova, batizada de “cohomologia de magma”, que nem um especialista da área tinha visto antes. Para Tao, isso comprovou o que ele queria demonstrar: que esse jeito de fazer matemática, experimental, decentralizado, verificado por máquina, produz descoberta real, e não é só um exercício de organização.

O que essa mudança de método pede de quem pesquisa

Quando li sobre o percurso de Tao, o que mais me chamou atenção não foi a tecnologia em si, foi a disposição dele de aprender algo do zero mesmo já sendo a maior autoridade do campo. Ele levou quase um mês para formalizar uma prova de dez páginas que na versão em papel ele escreveu em pouco tempo. Isso contraria a ideia de que uma ferramenta nova já entrega ganho de velocidade de cara.

Por outro lado, a matéria mostra que o ganho não veio da ferramenta isolada, veio de reorganizar o trabalho em torno dela: lemas pequenos, tarefas modulares, muita gente contribuindo com pedaços que se encaixam. Isso é organização de projeto, não mágica de IA. Um colega de Tao, o matemático Johan Commelin, fez uma ressalva importante durante o próprio projeto: contribuir para formalização ainda não é reconhecido do mesmo jeito que autoria de artigo na hora de avaliar currículo acadêmico. Vale ter isso em mente antes de investir tempo pesado numa ferramenta nova sem saber como ela vai contar no seu processo de avaliação.

Próximos passos

Se essa combinação de IA e verificação formal interessa ao seu tipo de pesquisa, aqui vai por onde começar a olhar:

1. Identifique se o seu problema de pesquisa pode ser quebrado em subtarefas pequenas e paralelizáveis. Foi isso que tornou os dois projetos de Tao viáveis.
2. Antes de adotar qualquer ferramenta de verificação ou IA generativa no seu fluxo, pergunte à sua orientadora ou à sua banca como essa contribuição seria avaliada.
3. Trate a saída de modelos de linguagem como hipótese a testar, não como resposta pronta, principalmente em problemas com pouco dado disponível.
4. Acompanhe como sua área está lidando com verificação automatizada de resultados: o caso de Tao mostra um caminho possível nesse sentido, mas a lógica de dividir, testar e verificar se aplica a qualquer pesquisa baseada em dados.

Se você quer entender melhor os limites éticos de usar IA generativa na sua própria produção científica, vale ler A ciência está mais inteligente ou mais artificial com a IA?.

Fonte: How Terry Tao Became an Evangelist for AI in Math, Quanta Magazine