Em um comentário no Hacker News, o usuário Jake Boggan descreveu a sensação ambígua de descobrir que a Conjetura de Barnette — problema ao qual dedicou 24 anos de forma intermitente, aparece como supostamente resolvida em um repositório ligado à OpenAI. O desabafo foi destacado por Simon Willison em seu blog, em 7 de outubro de 2026, na seção em que o autor reúne citações que considera relevantes.
A suposta prova está registrada como problem 180 na documentação em Lean do projeto OpenAI/math.
Um problema de 24 anos
Boggan conta que foi um entusiasta de teoria dos grafos e que chegou a se mudar para Budapeste, na Hungria, para estudar entre os grandes nomes da área. Foi nesse período que começou a trabalhar na Conjetura de Barnette, problema que ocuparia seus pensamentos pelos 24 anos seguintes, em idas e vindas, enquanto ele transitava por áreas profissionais bastante diferentes.
No verão anterior ao comentário, chegou a acreditar por alguns dias que havia finalmente resolvido a conjectura.
Agora, ele diz ter encontrado a indicação de que o problema estaria provado em uma página do repositório OpenAI/math, no GitHub, mais especificamente no arquivo problem 180, que integra uma documentação voltada a demonstrações formalizadas em Lean, um assistente de provas usado para verificar passo a passo a validade de um argumento matemático.
A reação de quem dedicou milhares de horas
O comentário, publicado na discussão sobre o repositório OpenAI/math, está longe de ser uma comemoração. Boggan afirma não saber exatamente o que pensar diante da notícia.
Ele lembra que passou milhares de horas naquele problema e que gostou genuinamente do tempo investido. Saber que a questão teria sido resolvida o deixa triste de um modo distante, comparação que ele faz com a de receber a notícia de que uma ex-namorada morreu subitamente em um acidente de carro.
Ele acrescenta que provavelmente muita gente estaria sentindo emoções parecidas naquela noite.
O post de Willison é curto: ele reproduz o trecho do comentário e o arquiva sob etiquetas como matemática, IA, OpenAI, IA generativa, LLMs e deep-blue, esta última uma referência aos momentos em que máquinas superam humanos em domínios que pareciam inatingíveis, como ocorreu no xadrez. A escolha das etiquetas indica como o episódio foi enquadrado: não como uma nota técnica isolada, mas como um marco na relação entre sistemas de IA e pesquisa matemática.
Por que isso importa
O caso resume uma tensão cada vez mais presente na matemática e na ciência da computação: avanços obtidos com apoio de sistemas automatizados podem encerrar, de uma só vez, décadas de trabalho humano. O peso aqui vem do fato de que se trata de um problema que mobilizou uma pessoa por 24 anos, e não de um exercício artificial criado para medir desempenho.
Também chama atenção o formato escolhido para registrar a suposta prova: um arquivo dentro de uma documentação em Lean, ligada à verificação formal, e não um artigo tradicional submetido à revisão por pares.
Vale notar o que o material disponível não afirma. No trecho destacado, não há descrição de como a prova teria sido produzida, nem atribuição a um autor ou a um sistema específico, nem confirmação pública de que a conjectura foi de fato demonstrada.
O que existe é a indicação de prova no repositório e a reação de alguém que conhece o problema em profundidade, uma combinação que, por si só, já produziu um debate sobre o que significa resolver um problema matemático nos dias de hoje.
Para quem passou anos vivendo um problema aberto, a notícia de uma solução tem um efeito curioso: encerra uma relação pessoal antes mesmo de qualquer verificação comunitária. Boggan não questiona publicamente a validade do resultado; ele descreve o que sentiu ao vê-lo.
É essa dimensão humana, mais do que qualquer detalhe técnico, que fez o comentário circular e chegar ao registro de Willison no dia 7 de outubro de 2026.
Fontes e links
- Simon Willison
- Comentário de Jake Boggan no Hacker News
- Repositório OpenAI/math
- Problem 180 na documentação em Lean
