A Anthropic colocou no GitHub o repositório público zeta-23-lean, uma formalização em Lean 4 de resultados avançados sobre zeros da função zeta de Riemann, e isso muda o patamar de transparência matemática em volta da IA da empresa.
Adicione ao Google NotíciasNeste artigo
O GitHub: anthropics cria o repositório "zeta-23-lean" aparece no site da Anthropic como um “research artifact” estático, que acompanha o paper "More than two thirds of the zeros of the Riemann zeta function lie on the critical line" (Claude; Anthropic, San Francisco, 2026). O código traz uma prova completa, sem sorry, dos Teoremas A–E do artigo dentro do ecossistema Lean 4/Mathlib, com auditoria explícita de axiomas usados pelo kernel.
O que é o zeta-23-lean e o que ele prova exatamente?
O repositório zeta-23-lean aparece no GitHub da Anthropic como público, sob licença Apache 2.0, com 9 commits, 11 forks e 117 estrelas registrados, e é classificado pela própria empresa como “Research artifact. Not maintained and not accepting contributions.” Ou seja: nada de PR aberto, nada de usar isso como biblioteca viva; é o snapshot congelado da prova formal que acompanha o paper assinado por Claude.
No coração do repositório está uma formalização Lean 4/Mathlib dos Teoremas A–E do trabalho "More than two thirds of the zeros of the Riemann zeta function lie on the critical line". A Anthropic afirma que o código cobre, entre outras coisas, versões formais de:
• Teorema A: as funções de contagem de zeros N(T₁,T₂) e N₀*(T₁,T₂) são tratadas em Lean, e o resultado formalizado garante que o liminf de N₀*(T,2T)/N(T,2T) e de N₀*(T)/N(T) é pelo menos 2/3.
• Teorema B: ao menos dois terços dos zeros são simples e estão na linha crítica, tanto em janelas diádicas quanto cumulativas.
• Teorema C: o liminf de N_d/N, onde N_d conta zeros distintos, é pelo menos 5/6.
• Teorema D: com a janela ótima de Montgomery–Taylor, aparecem constantes refinadas: 0,67250… para proporção de zeros na linha crítica e 0,83625… para zeros distintos.
• Teorema E: versões análogas de A–D para L-funções associadas a caracteres de Dirichlet primitivos χ modulo q > 1.
Segundo o README, tudo isso é construído diretamente a partir de definições de riemannZeta e analyticOrderAt da Mathlib. As declarações topo de pilha não assumem hipóteses adicionais, o repositório não introduz axiomas novos e um #print axioms em cada teorema principal retorna apenas os três axiomas padrão do Lean: propext, Classical.choice e Quot.sound. Para quem trabalha com formalização, é o tipo de controle de dependência que normalmente dá trabalho para reconstituir.
Qual a ferramenta usada e como esse repositório conversa com o resto da Anthropic?
O zeta-23-lean é construído sobre Lean v4.33.0-rc2 e um commit específico da Mathlib (hash 51e6992efd06126df61a496bebf8f49482a4e129, identificado como v4.33.0-rc2 no lake-manifest.json). O repositório inclui arquivos de configuração (lakefile.toml, lake-manifest.json, lean-toolchain) que travam exatamente a toolchain usada, o que é fundamental para quem quer reproduzir as provas anos depois sem cair em incompatibilidades silenciosas de biblioteca.
Do ponto de vista de produto, isso se encaixa no portfólio mais amplo da Anthropic no GitHub. A mesma organização hospeda hoje desde SDKs oficiais (anthropic-sdk-python, anthropic-sdk-go, anthropic-sdk-typescript, entre outros) até ferramentas de uso diário com Claude, como o agente de terminal claude-code, ações para CI (claude-code-action, claude-code-base-action) e diretórios de plugins (claude-plugins-official, claude-plugins-community, knowledge-work-plugins). Há ainda repositórios de skills específicos, como skills (Agent Skills genéricos), defending-code-reference-harness (skills focadas em segurança) e k12-teacher-skills.
Isso importa para quem olha para "official anthropic skills" e "skills para Claude Code" porque a Anthropic deixa explícito um pipeline que vai da matemática dura até o produto. O zeta-23-lean vira o contraponto teórico de coisas mais pé no chão como claude-code e os repositórios de skills MCP: o mesmo Claude que aparece como autor do paper é a marca em cima das ferramentas que os devs já usam no terminal.
Que extras o repositório traz além dos Teoremas A–E?
O README lista uma quantidade razoável de resultados que vão além dos Teoremas A–E, todos formalizados no mesmo ambiente Lean 4/Mathlib e organizados em subdiretórios. Dois blocos chamam atenção.
O primeiro é o pacote sobre as zeros da derivada ξ′ da função zeta completada. Em Zeta23/XiPrime/, o repositório oferece seis declarações, incluindo afirmações de que, incondicionalmente, ao menos 0,85838 dos zeros de ξ′ em janelas (T,2T] são simples e estão na linha crítica, e 0,92919 são distintos (valores que sobem para 0,86864 / 0,93432 com a chamada janela quártica). Também aparece o resultado de que todos os zeros de ξ′ estão na faixa crítica aberta, e que Re ξ′/ξ > 0 para Re s ≥ 1. A Anthropic conecta isso a um argumento inspirado em Farmer–Gonek (e Farmer–Gonek–Lee), com referências diretas a um suplemento técnico externo, mas deixa claro que o que vale para o sistema é a versão Lean do enunciado.
O segundo bloco é a tal bandwidth-one ceiling, em Zeta23/PairCeiling/. Ali aparece uma desigualdade de estabilidade para certificados do tipo usado no Teorema B, escrita em termos de uma função r em C¹[0,1] com hipóteses sobre derivadas e integrais. A conclusão, ainda segundo o README, é um limite explícito para o que qualquer certificado de banda 1 consegue provar sobre a fração de zeros simples: algo na forma de 0,6818287 + 2,55·10⁻⁶·(|r′(1)| + ∫|r″|). O detalhe curioso é como os dados de entrada (medidas de fator de forma S(j), j = 1…256) vêm de um certificado racional gerado fora do Lean, registrado por um hash SHA256, e depois verificado no kernel via decide. É o tipo de engenharia de verificação que normalmente fica escondida em anexo de paper, e aqui aparece traduzida em código legível.
O repositório ainda inclui um arquivo comparator/config.json e módulos sob comparator/ dedicados a um conjunto de quinze declarações mais fracas (como versões Cauchy–Schwarz dos Teoremas B–E: N₀ˢ/N ≥ 1/2, N_d/N ≥ 3/4, e janelas com constante 2c₁* − 1 ≈ 0,5065). A Anthropic usa isso para mostrar como diferentes configurações cobrem regiões do espaço de parâmetros, algo que interessa a quem pensa em reusar a técnica para outros problemas, mesmo que o repositório oficialmente não aceite contribuições.
No fundo, o zeta-23-lean escancara um pedaço da aposta da Anthropic: associar o nome Claude a resultados matemáticos formalmente verificados, com código aberto auditável, em vez de deixar tudo escondido atrás de um PDF e de uma demo de chat. Resta ver quantos times de pesquisa independentes vão efetivamente rodar essa toolchain de Lean 4.33 para conferir cada detalhe — e quantos vão só apontar para o GitHub e assumir que, se compila sem sorry, está certo.
