GPT-5.6 Sol Ultra produz prova da Conjectura da Cobertura Dupla por Ciclos [pdf]

Validade e verificação da prova

• Muitos estão entusiasmados, mas cautelosos: a prova é curta, usa teoria dos grafos anterior aos anos 1990 e parece plausível, mas pode conter erros sutis.
• Alguns argumentam que ela deveria ter sido anunciada por matemáticos profissionais ou após formalização em Lean / revisão por pares em periódico.
• Outros observam que a OpenAI publicou um repositório de formalização em Lean, mas as bibliotecas de teoria dos grafos ainda são imaturas, então mecanizar isso não é trivial.
• Vários comentaristas tentaram fazer outros LLMs e ferramentas verificarem a prova; em geral relatam não encontrar erros óbvios, mas ressaltam que isso não substitui uma revisão especializada.
• Pelo menos uma preocupação técnica levantada no Reddit é argumentada no próprio fio como sendo um problema de notação, não uma falha fatal. O veredito geral: promissora, mas ainda não universalmente aceita.

Prompting, harness e consciência de tempo

• O prompt divulgado é fortemente metarreflexivo: instrui o modelo a assumir que uma prova existe, trabalhar por pelo menos 8 horas, evitar relatórios de status vagos e explorar múltiplas estratégias.
• Comentadores veem isso como “motivation hacking” e orientação metaheurística, em vez de autonomia pura.
• Há discussão sobre rastreamento de tempo em harnesses de agentes (carimbos de data/hora, date do SO, ferramentas de quota) versus a falta de senso temporal inato dos modelos.
• Sol Ultra é descrito como muitos subagentes paralelos com raciocínio máximo, diferente da abordagem “best-of-N” do Sol Pro.

Opacidade metodológica e viés de sobrevivência

• Vários comentaristas perguntam quantos problemas e variantes de prompt foram tentados, e quantas execuções fracassadas precederam esse sucesso.
• Há especulação de que a OpenAI vem rodando muitos problemas desde o resultado anterior de distância unitária; a ausência de uma “taxa de falha” torna difícil medir a capacidade.
• Há preocupação de que empresas destaquem sucessos raros para marketing enquanto enterram resultados nulos.

Significado para a matemática e para assistentes de prova

• Alguns veem isso como um grande marco: um modelo pronto para uso resolvendo um famoso problema em aberto em menos de uma hora.
• Outros apontam que é uma prova do tipo “truque esperto”, não uma descoberta de longo alcance que constrói teoria; argumentam que a próxima barreira é o desenvolvimento autônomo de teoria substancialmente nova.
• Há forte apoio a avançar para verificação formal no estilo Lean para lidar com grandes volumes de provas geradas por IA e reduzir gargalos de checagem humana.

Implicações mais amplas e ansiedades

• Debate sobre quais tarefas são mais automatizáveis: qualquer coisa com correção facilmente verificável (matemática, código, segurança, alguma ciência) pode ser especialmente vulnerável.
• Discussão filosófica sobre o valor da matemática pura, se resultados gerados por IA “parecem vazios”, e o que permanece exclusivamente humano (criação de conjecturas, gosto, explicação, responsabilidade).
• Alguns expressam preocupação com empregos, valor humano e hype da IA; outros respondem que o valor humano não está ligado à produtividade econômica e que ferramentas irão ampliar, e não apagar, as pessoas.