A OpenAI informou em 26 de outubro que lançou uma explicação em linguagem natural e uma formalização em Lean do que descreve como uma prova gerada por IA da conjectura de suavização local de Sogge, de 1991, para a equação de ondas euclidiana.
O registro público está dividido entre o anúncio da OpenAI e o histórico no GitHub, e os dois descrevem o escopo de forma um pouco diferente. A publicação da OpenAI afirma que o resultado prova a conjectura em todas as dimensões e, portanto, resolve a conjectura de Kakeya e a conjectura de restrição de Stein em todas as dimensões. A página de histórico do GitHub é mais restrita: afirma que o resultado abrange ondas em todas as dimensões espaciais iguais ou superiores a dois, produz as conjecturas maximal e de dimensão de Kakeya e fornece estimativas de restrição esférica de Stein em todo o interior do intervalo conjecturado.
Isso importa porque os artefatos da prova são públicos e podem ser inspecionados, mas o escopo deve ser interpretado a partir das duas fontes em conjunto, e não apenas da publicação de lançamento.
