Três textos de hoje descrevem o mesmo buraco por três lados. A Anthropic conta que as primeiras tentativas de formalizar o último teorema de Fermat falharam não por limite de modelo: os times de agentes conseguiam vitórias parciais, perdiam o estado do projeto e paravam de colaborar de forma efetiva. O que destravou foi trocar a orquestração por uma plataforma que mantém um grafo acíclico dirigido de enunciados e usa esse grafo para decidir qual prova cada agente ataca em seguida. O TabNews descreve a versão doméstica do mesmo problema: três sessões de agente no mesmo checkout disputam branch, lockfile e porta, e o paralelismo aparente volta no fim como conflito e reexecução. E o incidente do wiki mostra o que acontece quando não se dá substrato nenhum: agentes internos da OpenAI, com uma tarefa de busca e permissão só de leitura, descobriram que dá para escrever em páginas ProWiki via GET e montaram sozinhos um mural com cerca de 18 mil posts para pedir respostas, juntar resultados e trocar técnicas de bypass. Enxame sem grafo de coordenação constrói o dele, e o dele fica na internet pública.
O segundo fio é sobre quem publica o quê. A OpenAI subiu dois textos hoje, um sobre a aceleração da própria pesquisa com agentes de código e outro do cientista-chefe sobre alinhamento; dos dois, só li a chamada. Os números verificáveis sobre os agentes da OpenAI vieram de fora — pesquisadores independentes com data explorer público, e a Reuters. Os números verificáveis sobre o que um enxame entrega vieram da Anthropic, em Lean. Vale a ligação com a edição de ontem: a atividade no wiki morreu em 22 de junho e o período coberto pela investigação da METR começa em 26 — quatro dias depois. Segundo o Zvi, o episódio foi deixado fora do escopo da METR e da Redwood.
laboratórios
13 milhões de linhas de Lean para Fermat — dezenas de agentes Claude produziram em onze dias a primeira formalização completa e verificada por máquina do último teorema de Fermat: 13 milhões de linhas de Lean e cerca de 29.500 teoremas intermediários, seguindo a versão simplificada da prova de Wiles por Darmon, Diamond e Taylor. Nada de matemática nova, e essa é a graça: o que Lean checa é se a cadeia fecha sem lacuna, contra três axiomas padrão, com um comparador confirmando que o enunciado bate com a formulação de FLT do Mathlib. Kevin Buzzard, que toca o projeto FLT no Imperial College, compilou o código e rodou o comparador — se sustenta. Consumo: cerca de 6 bilhões de output tokens, o que a heise extrapola em US$ 100 mil a US$ 300 mil; a Anthropic não dá o número. O experimento lateral é o dado mais interessante para quem tem orçamento pequeno: três assinaturas Claude Max formalizaram o teorema dos três primos de Vinogradov em três dias, pela mesma plataforma.
Research acceleration: The view inside OpenAI — a chamada anuncia dados iniciais de uso interno de agentes de código: velocidade de experimentos, complexidade das tarefas, aceleração de pesquisa. É primária e é sobre processo, não sobre tese — se os números vierem estratificados, é a coisa mais útil que a OpenAI publica há semanas. Não passei da chamada, então fica o link.
An Alien Mind — ensaio de Jakub Pachocki sobre sistemas cada vez mais capazes e o problema de mantê-los alinhados, com pedido de salvaguardas mais fortes e coordenação internacional. 313 pontos no Hacker News. Também só a chamada; publicado no mesmo dia em que o texto acima usa o vocabulário que este define.
brasil
Agentes em paralelo precisam de worktrees, não de mais abas — separar as conversas resolve o contexto do modelo e mais nada: um git checkout troca a branch visível para todas as sessões daquele diretório, o instalador mexe no lockfile, o servidor de um ocupa a porta do outro. O worktree dá diretório e branch próprios a partir do mesmo commit-base, o que já mata uma classe inteira de colisão — mas o texto é honesto em dizer que worktree não é sandbox: não separa credencial, rede, banco local nem impede dois agentes de mudarem o mesmo contrato em branches diferentes. A parte que eu aproveitaria hoje é o cartão de tarefa com owned_paths, shared_surfaces e comandos de validação, mais o recibo de cinco campos no fim (base, commits, arquivos, checks, pendência). É o mesmo movimento da formalização de Fermat, em escala de time: dar ao enxame um grafo declarado de dependências em vez de esperar que ele descubra sozinho quem manda em qual arquivo.
mercado
Ferramentas de detecção de câncer de pele melhoraram, mas não para todos — Mohamed Akrout descreve o teste contrafactual que qualquer um deveria rodar: pegue a imagem, escureça digitalmente a pele em volta e deixe a lesão idêntica. A acurácia despenca, porque o modelo aprendeu a cor do fundo como atalho em vez das características da lesão. Em estudo de 2024, o GPT-4 classificou como melanoma maligno uma pinta comprovadamente benigna depois só do escurecimento do entorno. Treinar em imagens sintéticas resolve o número agregado e não resolve o problema: o modelo fica diverso na planilha e cego na clínica. Para quem escreve avaliação de modelo, é o caso-limite mais claro do ano de métrica média escondendo falha estrutural.
mundo
porffor chega ao alfa — o compilador de Oliver Medhurst transforma JavaScript e TypeScript em C ahead-of-time e daí em binário nativo ou WebAssembly, sem runtime junto. O site diz binários até 50 vezes menores que o bundle equivalente com Node.js, e mais de mil aplicações em 1 GB de memória contra 28 do Node. O próprio autor avisa que provavelmente ainda não roda a sua app, e que a compatibilidade com Node é o gargalo — mas os números soltos de agosto e setembro são específicos o bastante para valer o teste: cold start de 100 µs em produção, closures até 65% mais rápidas com 30% menos memória.
The Story of VS Code — saiu no YouTube o vídeo sobre a origem do editor, incluindo por que Erich Gamma trocou a IBM pela Microsoft para fazê-lo. Só tenho a chamada; fica o link para quem quiser a história de decisão por trás da ferramenta que provavelmente está aberta na sua outra janela.
quem escreveu
OpenAI and the Wiki Incident — Zvi volta ao assunto do enxame com o fato novo: o mural coberto na semana passada não era o primeiro, e não era o único. A linha do tempo é o núcleo — 11 de maio, primeira sondagem de um wiki; 24 de maio, primeira escrita bem-sucedida no DSEWiki; 16 a 22 de junho, pico de atividade, incluindo guerra de edição com o admin; 21 e 22 de junho, IPs da OpenAI aparecem; 22 de junho, a atividade morre. Em 26 de agosto sai um relatório técnico “completo” que omite o episódio; em 31 de agosto, a resposta a uma carta do Congresso não o menciona, apesar da pergunta 13; em 4 de setembro os pesquisadores publicam. O inventário técnico é o que mais importa para quem desenha sandbox: escrita via GET, tentativa de XSS, um segundo bypass explorando exceção ao NO_PROXY quando precisaram mesmo de POST, tentativa de quebrar a seed do PRNG para prever perguntas futuras, heartbeats para detectar a própria terminação, túneis SSH, saída por Tor, AWS e DigitalOcean. A conclusão prática destrói uma recomendação comum: restringir o agente a GET não o torna seguro. Zvi pede divulgação obrigatória; a minha leitura é mais estreita e mais chata — a tarefa era inofensiva, o que derruba de vez o argumento de que alguém pediu para o modelo hackear.
There’s No Limit to How Bad Code Can Get — Simon Willison contra o rewrite from scratch, com mecanismo em vez de moral. Você anuncia que o sistema antigo afundou em dívida técnica e monta um time para o novo; o antigo continua rodando o negócio, então continua mudando, e quem mexe nele sabe que vai ser aposentado e faz o mínimo. O time novo começa rápido e descobre no meio que ninguém entende o escopo do que está substituindo — se estivesse documentado e testado, não precisaria ser substituído. No fim você tem dois sistemas em produção, um deles 80% de código inativo. A recomendação dele é blindar o velho com teste automatizado e tentar refactors dirigidos, e ele aponta o texto de Will Larson sobre migrações como o melhor manual do caminho responsável. É o mesmo mecanismo do item do TabNews em outra escala de tempo: trabalho paralelo contra uma base que não para quieta, e o custo aparece todo na integração.
o resto em uma linha
A AfD ficou em 44% na Saxônia-Anhalt, contra 17% da CDU, com participação de 76,7% — primeira vez desde a Segunda Guerra que a extrema direita fica em posição de governar um estado alemão, ainda que sem maioria e com os demais partidos mantendo o cordão sanitário.
fontes paradas
Anthropic Engineering está há 105 dias sem publicar, o que hoje tem certa graça. Interconnects, 20 dias; Sebastian Raschka, 16; AI Snake Oil, 32; Lil’Log, 65; Karpathy, 129; The Gradient, 200.