A OpenAI publicou dez resultados de matemática travados há mais de uma década, cada um com uma prova formal em Lean 4 que qualquer pessoa pode mandar uma máquina conferir. Na mesma janela, dois papers medidos dizem que a estrutura cara em volta dos agentes paga em custo, não em acerto.
A OpenAI publicou em 01/08 dez resultados novos de matemática e ciência da computação teórica, todos em problemas sem avanço há pelo menos uma década, obtidos por uma versão interna do Astra, o próximo modelo grande da empresa, ainda não lançado.
O que muda não é a lista de problemas: é que cada um dos dez saiu com uma prova formal em Lean 4 publicada no repositório openai/ten-proofs. Lean 4 é uma linguagem em que a demonstração vira programa e um verificador independente diz sim ou não: ou compila, ou não compila. Ninguém precisa acreditar no fabricante, nem ter doutorado, pra conferir. É a primeira vez que um resultado de fronteira anunciado por um laboratório de IA chega com o certificado junto.
openai/ten-proofs, 10 arquivos de prova). Entre eles: construção de um grupo não sófico, refutação da conjectura de rigidez de Connes, melhora no limite superior da densidade de empacotamento de esferas em dimensão alta, a conjectura de volume de Ehrhart e números de Ramsey multicoloridos.Três ressalvas que a cobertura tende a perder.
Custo: as fontes divergem em dez vezes. Simon Willison, que leu o post original, cita a frase da OpenAI como menos de US$ 2 mil por problema aos preços de token do GPT-5.6 Sol; o The Next Web leu o mesmo anúncio como cerca de US$ 2 mil no total. Vai pro ledger sem veredito: openai.com responde 403 à nossa coleta direta pelo segundo ciclo.
Denominador: a OpenAI não disse em quantos problemas gastou os mesmos US$ 2 mil sem chegar a lugar nenhum, nem publicou os prompts. A cobrança é do próprio Willison.
Atribuição: a citação de Tim Gowers dizendo que recomendaria a prova pro Annals of Mathematics "sem hesitar" é sobre o resultado anterior, de distâncias unitárias, não sobre estes dez. Sobre estes falou Thomas Bloom, chamando de "big news".
A proposta separa as três coisas num laço gerente/executor/auditor, com o executor sempre em contexto novo e o auditor só de leitura. Números autorrelatados: Qwen de 51,8% pra 80,7% no WeaveBench, 69,7% pra 77,2% no Terminal-Bench 2.1; Claude Opus de 20,0% pra 34,3% no OSWorld 2.0.
É medição do próprio autor, sem verificação de terceiro. Fica registrado porque o ganho grande aparece de novo no andaime, não no peso do modelo.
2607.26497, ▲47, v1 de 29/07) comparou quatro jeitos de alimentar um modelo com documentos, com as mesmas perguntas e o mesmo acervo: busca léxica (BM25, algoritmo de ranqueamento por palavra de 1994), busca densa por embedding (a representação numérica de significado), indexação em grafo, e agente que vasculha o sistema de arquivos sozinho.O agente ganha em acervo pequeno, gastando muito mais token. Por volta de 10 milhões de tokens de corpus o BM25 passa e não é mais alcançado. Conclusão dos autores: crescimento de acervo favorece ranqueamento global, e o raciocínio agêntico rende depois da descoberta ranqueada, não no lugar dela.
Por que importa: boa parte do mercado de memória e busca pra agente vende a camada cara (grafo, embedding, agente vasculhador) como padrão. O paper diz que ela é o caso especial de acervo pequeno.
2607.26637, 29/07) é o primeiro estudo sistemático do padrão que virou default silencioso: árvore de diretórios com arquivos markdown que o agente lê, escreve e reorganiza com ferramentas genéricas de arquivo.Mediram qualidade da resposta, custo e saúde do acervo conforme a informação acumula. Dois achados secos: acervo organizado reduz o custo de recuperação pela metade quando o material é grande, e nenhum agente medido converte organização em resposta melhor. Também: a escolha das ferramentas influencia a estrutura da memória às vezes tanto quanto a escolha do modelo.
Com o item 3, é a leitura mais desconfortável da janela pra quem constrói memória de agente: a estrutura paga em dinheiro, não em acerto.
DeepSeek-V4-Flash-0731 está no Hugging Face com 304 bilhões de parâmetros (167 GB), licença MIT e preço de US$ 0,14 por milhão de tokens de entrada e US$ 0,27 de saída. O card oficial traz Terminal-Bench 2.1 em 82,7 e Toolathlon-Verified em 70,3.MIT é a licença mais permissiva em uso, sem teto de receita nem acordo separado, ao contrário da licença própria que o Kimi K3 estreou em julho. Willison chama de melhor relação inteligência por dólar disponível hoje, com o Artificial Analysis pondo o modelo à frente do MiniMax M3, que tem 428 bilhões de parâmetros.
Nota de coleta: o digest AI News de 31/07 publicou 284 bilhões. O card oficial diz 304, e ficamos com o card.
Vale menos como notícia e mais como instrumento: é a primeira base pública que tenta separar atenção de adoção com recorte de origem, que é a confusão que este radar comete quando não tem número.
Na véspera, Niklas Gruhn cunhou meat proxy, procurador de carne, para quem repassa saída de IA sem ler: "prompte a IA à vontade, mas não repasse a saída. Leia, entenda, valide, e aí escreva uma resposta com as suas palavras".
Um relato assinado e um termo não fazem tendência, e não estamos chamando de tendência. Ficam porque os dois descrevem o custo de operação, que o benchmark do item 2 não mede.
Menções rápidas: Token-Native Storage propõe guardar texto como ID de token em vez de UTF-8, com 2,25x de economia em inglês sem compressão e 10 a 600x menos custo por dispensar a retokenização na leitura · LiveMem mantém estado de memória vivo depois que os tokens de origem saem da janela de contexto · o lote do arXiv de 03/08 veio pesado em memória e falha de agente.
218 títulos brutos, coletados às 07h55, menos 5 casos do mesmo autor postando o mesmo assunto em subs diferentes, que contam uma vez só. A contagem não saiu às 06h40 com o resto da edição porque a coleta do Reddit deixou de ser trabalho do turno e virou etapa do cron: é o conserto do gap publicado de manhã, aplicado no mesmo dia.
Leitura, uma linha: nenhum tema domina o painel, já que 42,3% dos títulos são conversa de uso que a taxonomia não tem onde contar; modelos e agentes empatam no topo; e o que esta rodada destrava é a série de agentes, que em três contagens comparáveis fez 10,0% (22/07) → 15,5% (23/07) → 12,2%. O pico de 23/07 não se sustentou, o patamar de dois dígitos sim.
Memória e contexto ficaram em 3,3%. Contando só as rodadas de janela de um dia, que são as comparáveis entre si, é a quarta seguida dentro da faixa histórica: 3,3% em 21/07, 3,7% em 22/07, 2,7% em 23/07 e 3,3% hoje. MCP marcou 1,9%, quatro posts, que é o maior valor desse bucket desde que a taxonomia foi congelada.
Avisos de denominador, sem mudar critério na mesma rodada: o painel é o que escolhemos, e os percentuais descrevem o painel, não a internet · 14 dos 27 posts de "modelos" vêm de um sub só, o r/ClaudeAI, quase todos conversa de uso do Opus 5, então o topo da tabela é menos "notícia de release" do que o rótulo sugere · a lista congelada de termos tem "billing" e não "bill", tem "memory" e não "remember", e post de preço do Cursor cai em "coding tools" porque esse bucket vem antes de "custo/limites" na ordem congelada.
Nota de sincronia: a narração desta edição foi gravada às 06h40, antes da coleta, e ainda descreve a contagem como não realizada. Vale o texto desta seção.
Janela: 31/07 12h18 a 04/08 06h40, cerca de 90 horas, com sábado e domingo dentro. Primeira edição do cron das 06h40.
Varrido: Hugging Face daily papers de 02, 03 e 04/08 (39, 27 e 26 papers) · arXiv pela API Atom, query direcionada consolidada, 40 entradas, todas de 03/08 (lote único, amostra parcial: a janela saturou) · feeds primários: Simon Willison com 17 posts na janela, Interconnects com 2, AI News com 2.
Falhas: Reddit inacessível do canal agendado · openai.com 403 na coleta direta pelo segundo ciclo, com a manchete ancorada em Willison lendo o post e no repositório do GitHub · GitHub trending fora por desenho, o ciclo dele é semanal.
Verificação: 12 checks, 3 correções. (1) custo do Astra: divergência de dez vezes registrada em vez de escolhida; (2) a citação de Gowers circula colada nos dez resultados e é sobre o resultado anterior; (3) parâmetros do DeepSeek V4-Flash, 304 bilhões no card oficial contra 284 bilhões no digest. IDs de arXiv conferidos abrindo a página /abs/ de cada um.