GPT-5.6 usou um prompt para fechar uma lacuna de 30 anos em otimização convexa
Um modelo de IA (GPT‑5.6 “Sol Pro”) ajudou a provar um resultado em aberto de 30 anos em otimização convexa, usando um prompt especializado de dez páginas e uma prova posteriormente verificada no provador de teoremas Lean. Os comentadores debatem quanta novidade genuína o sistema contribuiu em comparação com agir como um assistente automatizado extremamente poderoso, e o que isso implica para o futuro papel de matemáticos e programadores, especialmente em problemas de “fruta baixa” e “média”. A discussão se amplia para questões sobre se grandes modelos de linguagem são apenas “papagaios estocásticos”, quão rapidamente podem deslocar o trabalho humano em várias áreas e que tipos de mudanças sociais e econômicas seriam necessárias se a IA continuar avançando.
Escopo do resultado e como ele foi obtido
- Comentadores observam que a prova foi verificada em Lean, mas ainda não foi revisada por pares, então seu status é “promissor, mas provisório”.
- A nuance principal: GPT‑5.6 Sol Pro usou um prompt de cerca de 10 páginas, elaborado por um especialista na área e baseado em um ano de trabalho humano prévio (incluindo tentativas anteriores assistidas por LLM).
- Isso é visto como uma forte evidência de que LLMs podem fechar lacunas quando o caminho é alcançável com técnicas já existentes, mas não como autonomia do tipo “digite ‘resolva isto’ e vá embora”.
Implicações para matemática e carreiras de pesquisa
- Alguns argumentam que os frutos baixos e “médios” em matemática/TCS serão cada vez mais transferidos para a IA, deixando os humanos focarem em ideias verdadeiramente novas e na seleção de problemas.
- Outros se preocupam que isso enfraqueça os caminhos tradicionais de formação, em que juniores aprendem justamente com esse tipo de problema.
- Vários comparam isso ao software: juniores e “seguidores de receitas” podem ser deslocados primeiro; compreensão profunda de domínio e de sistemas ainda importa.
LLMs: inteligência, criatividade e o debate do “papagaio estocástico”
- Entusiastas dizem que resolver problemas de 30 anos e contribuir para outras conjecturas refuta a visão de “mero papagaio” e mostra raciocínio genuíno.
- Céticos mantêm que LLMs são motores sofisticados de previsão baseados em padrões gerados por humanos, e não verdadeiramente criativos nem dotados de compreensão.
- Alguns sugerem que, se isso não é “inteligência”, a palavra perde o sentido; outros respondem que correspondência estatística de padrões mais busca por força bruta pode explicar o resultado.
Prompting, agentes e “engenharia de harness”
- Vários comentários enfatizam que escrever bons prompts e processos está mais próximo de engenharia de processo/harness do que de “prompt mágico”.
- Há discussão sobre sistemas multiagente (Pro vs Ultra), em que modelos planejam, executam, testam e se autocríticam em ciclos.
- As pessoas observam que LLMs também podem ajudar a gerar seus próprios prompts e fluxos de trabalho, reduzindo com o tempo a necessidade de elaboração manual de prompts.
Verificação formal e infraestrutura de provas
- Lean é destacado como o análogo atual de sistemas antigos como Mizar; provas verificadas por máquina são vistas como cruciais para confiar em matemática gerada por IA.
- Alguns gostariam de ver LLMs enfrentando provas muito longas ou opacas (por exemplo, grandes teoremas de classificação) por meio de formalização completa.
Preocupações sociais e econômicas mais amplas
- As reações vão de entusiasmo (“inteligência é barata, podemos acelerar a ciência”) a ansiedade sobre perda de empregos, estratificação e futuros “tecnofeudais”.
- Vários argumentam que o verdadeiro problema é a economia política: como os ganhos são distribuídos, e não a matemática em si.