Matemático rejeita avanço de conjectura da OpenAI em 24 horas: 'A IA provou cada frase, mas não se trata mais da conjectura original'

A OpenAI afirmou que seu modelo de IA de próxima geração resolveu dez problemas matemáticos de classe mundial, incluindo a refutação da conjectura de rigidez de Connes. No dia seguinte, uma matemática humana respondeu com um artigo argumentando que o contra-exemplo da IA é inválido. A autora, J.L. Nielsen, do Centro de Física Topológica da Universidade do Kansas, rastreou as 37.000 linhas de código Lean 4 da OpenAI do início ao fim, mapeando cada objeto de volta ao seu protótipo matemático, e identificou dois caminhos de falha independentes. A conjectura de rigidez de Connes afirma que se dois grupos têm a mesma estrutura algébrica associada e satisfazem duas condições adicionais (ICC e a propriedade (T) de Kazhdan), então os grupos devem ser isomorfos. O modelo da OpenAI construiu dois grupos não isomorfos que geram a mesma álgebra, com provas de que ambos os grupos satisfazem ICC e a propriedade (T). Nielsen apontou que um dos grupos construídos pela IA na verdade não satisfazia as condições adicionais, não sendo nem ICC nem tendo a propriedade (T). Ela listou três razões possíveis: a representação da propriedade (T) no código não correspondia fielmente à definição original de Kazhdan; a prova só valia para parte do grupo, mas foi aplicada ao todo; ou o grupo no código não é o que o documento explicativo descreve. Nielsen também fez uma verificação linha por linha do código, listando o nome de cada objeto matemático e o número da linha em uma tabela de referência cruzada. Ela descobriu que os lemas usados para provar ICC se aplicavam a objetos após uma transformação dual, não ao grupo original com seus elementos centrais, portanto não cobriam diretamente os elementos críticos. Ela escreveu suas duas refutações como código Lean e as compilou sob Lean 4.32.2. A seção final do artigo discute o contexto mais amplo: o kernel Lean garante a correção formal, mas não se a afirmação realmente prova a conclusão pretendida. Citando Terence Tao, verificar uma prova verifica a afirmação formal em si, não seu alinhamento com a intenção, portanto a revisão humana não pode ser substituída. Auditorias anteriores de cinco benchmarks comuns do Lean encontraram 4.833 problemas, incluindo contra-exemplos, teoremas vazios e axiomas não confiáveis, todos verificados por máquina, com humanos posteriormente construindo contra-exemplos para mostrar que as afirmações provadas eram falsas. Nielsen escreveu que a formalização da OpenAI pode ter estabelecido corretamente todas as conclusões que afirma, mas o que ela não estabeleceu - e o que o kernel Lean não pode verificar - é se essas conclusões se relacionam com o texto da conjectura original. A conjectura de rigidez de Connes permanece em aberto.