- A parte não resolvida do problema de decomposição hamiltoniana proposto por Donald Knuth foi ampliada e resolvida com a colaboração entre humanos e IA
- O Claude encontrou uma solução para m ímpar, que foi batizada de “Claude’s Cycles”; depois, 996 de 11.502 ciclos foram generalizados para todo m ímpar
- Dr. Ho Boon Suan usou o GPT-5.4 Pro para produzir uma prova de 14 páginas para m par ≥ 8 e fazer a verificação computacional até m = 2000
- Dr. Keston Aquino-Michaels descobriu uma construção simples para m ímpar e par com um workflow multiagente com GPT e Claude
- Dr. Kim Morrison formalizou a solução de Knuth no assistente de prova Lean, completando um ecossistema colaborativo entre humanos, IA e ferramentas de prova
Colaboração ampliada na resolução do problema Claude’s Cycles
- A parte não resolvida do problema de decomposição hamiltoniana proposto por Donald Knuth foi resolvida com a colaboração entre humanos e IA
- Inicialmente, o Claude encontrou em cerca de uma hora de exploração uma solução para m ímpar, e Knuth a batizou de “Claude’s Cycles”
- No artigo atualizado, para o caso-base m = 3, existem exatamente 11.502 ciclos hamiltonianos, dos quais 996 se generalizam para todo m ímpar
- Knuth confirmou entre eles 760 decomposições válidas do tipo “Claude”
- No caso de m par, o Claude não conseguiu concluir, mas Dr. Ho Boon Suan usou o GPT-5.4 Pro para escrever uma prova de 14 páginas para m ≥ 8 e realizar a verificação computacional até m = 2000
- Em seguida, Dr. Keston Aquino-Michaels encontrou uma construção simples aplicável tanto a m ímpar quanto par por meio de um workflow multiagente usando GPT e Claude em conjunto
- Dr. Kim Morrison formalizou e verificou a solução de Knuth para o caso ímpar no assistente de prova Lean
- Como resultado, formou-se um ecossistema matemático colaborativo completo em que humanos, vários sistemas de IA e ferramentas formais de prova cooperam em paralelo
- Essa sequência de avanços mostra um novo modelo de pesquisa matemática que começou com a resolução de um problema por uma única IA e se expandiu para uma colaboração entre múltiplas IAs, humanos e assistentes de prova
- O artigo mais recente foi publicado no site da faculdade de CS de Stanford (www-cs-faculty.stanford.edu/~knuth/papers/)
1 comentários
Comentários do Hacker News
Eu sempre disse que a IA vai ganhar uma Medalha Fields antes de operar um McDonald's
A matemática parece difícil para os humanos como usar um martelo para apertar um parafuso
LLMs são fortes em exploração rasa, porém ampla, e estão descobrindo muitos novos padrões matemáticos
Prevejo que, no futuro, haverá uma transição dos LLMs para aprendizado por reforço no estilo AlphaGo baseado em árvores de sintaxe do Lean
Se der para codificar os “10 truques” usados pelos matemáticos em vetores latentes, acabou o jogo
Pensamos aplicando, por analogia geométrica, geometria algébrica a problemas de teoria dos números
Uma IA treinada em árvores do Lean talvez possa ter um sistema de intuição mais amplo que o humano
Como no caso mostrado pelo StockFish no xadrez, vale a pena estudar essa abordagem pela ótica da interpretabilidade mecanística (mechanistic interpretability)
Puxar truques da cartola é algo em que os LLMs já são bons
Mas a parte de representar o problema corretamente ainda é dos humanos, e isso é natural
Quero acrescentar minha própria versão: “a última profissão a ser automatizada será QA”
Esta onda tecnológica está nos fazendo repensar a essência do trabalho intelectual, e isso vai nos deixar mais afiados
Desde que aprendi o velho ditado do 4chan, “trolls trolling trolls”, passei a olhar interações na internet sempre com desconfiança
Eu já sentia que o Reddit tinha virado uma ‘internet morta’, e vendo esta thread agora já não dá mais para distinguir quem é bot e quem é humano
Por isso criei um serviço chamado RememberBuddy — um espaço para guardar percepções do dia a dia e não esquecê-las
A evolução da matemática com IA provavelmente vai seguir a trajetória que Greg Egan previu em seus romances nos anos 90
A essência da matemática não muda, mas o motivo do ‘por quê’ muda
Em Diaspora, de Egan, a descoberta matemática é descrita como garimpar joias numa mina de sal
Alguns buscam a beleza pura dessas joias, outros perseguem seu valor prático
Lugares como o instituto fundado hoje por Terence Tao já tocam esse futuro
No curto prazo, esse tipo de pesquisa vai melhorar muito a capacidade dos sistemas de IA de gerar informação precisa
Algumas pessoas acham que descoberta de conhecimento é apenas imitar comportamentos passados, mas eu não vejo assim
Se um especialista souber conduzir bem o modelo, a maioria dos problemas pode ser resolvida
O modelo é excelente como ferramenta para assumir o trabalho preguiçoso do especialista, mas em problemas complexos ainda existem pontos cegos
Vi parte do system prompt no artigo,
havia uma regra dizendo:
“atualize o plan.md imediatamente após executar qualquer exploreXX.py”
Fiquei curioso por que esse tipo de prompt melhora o desempenho em resolução avançada de problemas
Estamos chegando cada vez mais perto da visão do CEO da OpenAI de “inteligência por assinatura (intelligence as a subscription)”
Reduzir a troca de abas está sendo subestimado
Metade das ferramentas de IA não é uma questão de UX, mas uma luta para garantir estabilidade no acesso ao modelo
“Se você der a 100 macacos 100 armas e materiais de construção, eles vão construir uma casa ou assaltar um banco?”
Se esse resultado acontecer, eu gostaria de perguntar se isso seria um comportamento intencional
Vi este tweet