GPT-5.6 fechou um gap de 30 anos em otimização convexa — com um prompt

Quando li o artigo de Phillip Kerger no Medium, a primeira reação foi ceticismo. Há meses que vemos anúncios de LLMs a “resolver matemática”, desde o AlphaGeometry aos rumores do o1 a fazer curtas-metragens de raciocínio. Mas um problema concreto, congelado há 30 anos, resolvido com um prompt de 10 páginas, sem intervenção, numa só sessão? Isto é diferente.

Phillip Kerger é assistant teaching professor na UC Berkeley. O problema em causa: determinar o lower bound para a complexidade de oráculo de otimização convexa determinística de ordem zero (zeroth-order). Traduzindo: quantas vezes precisamos de perguntar “quanto vale a função neste ponto?” até conseguirmos encontrar o mínimo de uma função convexa, quando só podemos ver os valores, nunca o gradiente.

---

Um gap de 30 anos em números

O contexto técnico é mais acessível do que parece. Imagina que tens uma função de d variáveis: temperatura, pressão e tempo de processamento para minimizar o custo de fabrico de uma peça. Só podes escolher um ponto e receber o valor da função nesse ponto. Quantas avaliações são precisas para ter a garantia de encontrar a solução?

Em 1996, um algoritmo de Protasov mostrou que bastavam cerca de O(d²) avaliações, a menos de fatores logarítmicos (o upper bound). Durante 30 anos, ninguém conseguiu provar se esse número era mesmo necessário, ou se dava para fazer melhor. O melhor lower bound que existia era apenas Ω(d), um valor herdado de modelos de primeira ordem que assumiam acesso a gradientes.

O problema estava aberto. Num congresso em 2025 (a ICCOPT, por confirmar), Kerger ouviu alguém dizer: “não fazemos ideia de como resolver isto.”

---

O prompt que fechou o ciclo

Kerger trabalhou no problema esporadicamente durante um ano. Tentou com GPT-5.4, depois com GPT-5.5. Nada. Sessões longas de ida e volta entre ele e o modelo, a explorar abordagens, sem sucesso.

Depois do lançamento do GPT-5.6 Sol Pro, ele mudou de estratégia. Inspirou-se na metodologia que a OpenAI usou para provar a Cycle Double Cover Conjecture — o resultado que a empresa tinha publicado semanas antes como demonstração das capacidades do modelo. Escreveu um prompt de 10 páginas, que adaptava essa mesma estrutura ao problema de otimização.

Duas horas e meia depois, sem uma única intervenção de Kerger, o modelo tinha produzido uma prova completa.

“Parte de mim ainda espera ter falhado alguma coisa importante”, escreveu Kerger no Medium. “Não gosto da ideia de que um modelo de IA resolveu algo em que sou especialista, muito mais depressa do que eu alguma vez conseguiria.”

---

Porque é que a verificação em Lean é o verdadeiro protagonista

Aqui chegamos ao ponto que mais me interessa nesta história. Kerger não se limitou a receber a prova do modelo e publicá-la. Ele submeteu-a ao Lean, um sistema de verificação formal de provas matemáticas. O Lean percorre cada axioma, cada passo lógico, e confirma que a demonstração é válida. O check passou.

Num mundo onde os LLMs são mestres em bullshitting (para usar a palavra do próprio Kerger), a verificação formal deixa de ser um luxo académico para se tornar uma necessidade operacional. Se um modelo consegue gerar algo que parece uma prova em 2.5 horas, a diferença entre uma prova real e uma alucinação plausível é a diferença entre verificar em Lean ou não.

Isto não é teoria. A Google, a OpenAI, e outros laboratórios já estão a construir sistemas que geram ideias via LLMs e depois tentam prová-las formalmente. O objetivo é um “verifiable automatic math researcher”. Para resultados que podem ser formalizados (e a maioria dos resultados matemáticos recentes cabe nessa categoria), a verificação formal vai ter de se tornar padrão.

---

O que isto significa

Kerger colocou o GitHub público com o paper, a verificação em Lean, o prompt completo de 10 páginas e o chat inicial. Tudo está disponível para quem quiser verificar por si próprio. O paper tem um título seco: Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization: A Near-Quadratic Lower Bound from Exact Function Values.

O resultado concreto: um lower bound de Ω(d² / log(d+1)) para a complexidade de oráculo, a uma precisão da ordem de d^−1/2, que encosta ao upper bound de Protasov, de O(d² log(d+1) log(1/δ)), a menos de fatores logarítmicos. Ou seja, a complexidade é Θ̃(d²) e o gap de 30 anos fica fechado até fatores logarítmicos, e não necessariamente com «exatamente d² avaliações». Duas ressalvas: o artigo é uma preprint (arXiv 2607.13335) e ainda não foi revisto por pares; e o Lean verifica apenas o resultado do lower bound, não o upper bound nem as transferências que o artigo também apresenta.

Na discussão do Hacker News, um utilizador resumiu bem o sentimento geral: “Isto parece mais nicho do que a Cycle Double Cover Conjecture, mas representa uma contribuição real.” (citação por confirmar) E acrescentou que provar lower bounds é sempre mais difícil do que upper bounds, porque requer constraint de todos os algoritmos possíveis.

---

Recursos adicionais

• Medium article de Phillip Kerger
• GitHub com paper + verificação Lean
• Discussão no Hacker News
• Chat original no ChatGPT

---

O que fica depois disto

O que mais me marcou foi a honestidade do Kerger no final do artigo. Ele diz que espera ter falhado alguma coisa, porque a alternativa é que um modelo de IA resolveu em 2.5 horas um problema em que especialistas andaram às voltas durante 30 anos. E depois pergunta: quantos problemas abertos estão neste momento a ser trabalhados por investigadores que estão a um prompt de distância de uma solução?

Não sei a resposta. Mas acho que vamos descobrir mais cedo do que pensamos. Para quem trabalha em matemática, ciência da computação ou qualquer área que dependa de raciocínio lógico rigoroso: estás a preparar-te para um mundo onde a verificação formal é o padrão, e onde a geração de ideias pode vir de qualquer lado, inclusive de um modelo que trabalha enquanto tu dormes?