OpenAI diz que modelos formalizaram provas em Lean e reivindicam avanços em matemática, computação e física

A OpenAI anunciou em 26 de outubro que seus modelos internos produziram provas formalizadas em Lean — um verificador de teoremas — que, segundo a empresa, resolvem a conjectura do local smoothing (incluindo as conjecturas de Kakeya e de Stein), refutam o Exponential Time Hypothesis (ETH) e estabelecem provas de existência matematicamente rigorosas para certas teorias quânticas de campo em quatro dimensões.

Os artefatos em matemática e ciência da computação e as explicações em linguagem natural foram publicados no GitHub com provas em Lean que verificam cada passo lógico. Os materiais de teoria quântica de campos, porém, estão sendo retidos temporariamente. Um grupo liderado por David Gross prepara um texto técnico.

A OpenAI designou ‘shepherds’ acadêmicos independentes para orientar a verificação: Russell Impagliazzo, Ramamohan Paturi e Ryan Williams para a reivindicação sobre o ETH, e David Gross e outros físicos seniores para o trabalho em QFT. A empresa também se comprometeu a financiar e organizar oficinas para apoiar a revisão pela comunidade.

Especialistas alertam que a verificação em Lean apenas prova que uma afirmação formal decorre de certas hipóteses dadas, e não demonstra, por si só, que essa afirmação formal corresponde exatamente às conjecturas canônicas nem revela a proveniência dos dados de treinamento. Por isso serão necessários meses de checagem independente e decisão por periódicos e instituições.

Se confirmados, os resultados exigiriam reavaliações técnicas amplas: o ETH sustenta muitos resultados de dureza computacional em detalhe fino; as reivindicações sobre local smoothing e Kakeya mudariam fundamentos da análise harmônica; e provas rigorosas de QFT em quatro dimensões tocaríam problemas centrais da física matemática.