🎀 Terence Tao está a fazer parceria com a Math, Inc. 🎀 como o inaugural Veritas Fellow — para formalizar estimativas em teoria dos números. Na teoria analítica dos números, a literatura contém uma vasta rede de estimativas explícitas. Mas essa rede não é imediatamente interoperável. Na prática, os resultados vêm em três camadas: Estimativas primárias: Estas são entradas fundamentais, como regiões sem zeros para a função zeta de Riemann. Elas frequentemente dependem de cálculos substanciais e otimização numérica cuidadosa. Estimativas secundárias: Muitos artigos tomam uma entrada primária (por exemplo, uma região sem zeros) e a convertem em consequências reutilizáveis, como contar primos em intervalos curtos. Estas tornam-se blocos de construção essenciais usados em toda a matéria. Estimativas terciárias: Trabalhos adicionais aplicam então esses blocos de construção secundários a problemas de fronteira na teoria dos números, por exemplo, representar inteiros como somas de três primos. A dificuldade é que essas camadas não se atualizam de forma limpa ao longo do tempo. Um artigo terciário pode depender da melhor estimativa primária disponível na época. Mas anos depois, cálculos melhorados refinam a entrada primária, sem serem sistematicamente propagados através da cadeia secundária e terciária. Como resultado, o “mesmo teorema com constantes atualizadas” é frequentemente desconhecido. O objetivo é formalizar artigos-chave através dessas camadas e depois abstraí-los para que suas dependências se tornem explícitas, compostáveis e verificáveis por máquina. A visão a longo prazo é criar uma rede viva de implicações: quando uma estimativa primária melhora, cada implicação a montante é automaticamente atualizada. Isso transformará a literatura matemática em software modular. A teoria dos números é um caso de teste forte porque suas estimativas têm uma estrutura relativamente clara e um conjunto compartilhado de entradas e saídas padrão. Mas em muitas áreas, como PDEs, os pesquisadores constantemente gastam esforço em modificação: adaptando lemas e hipóteses, traduzindo entre estruturas incompatíveis, “encaixando peças quadradas em buracos redondos.” Uma rede de implicações compostáveis e verificadas por máquina visa diretamente essa fricção. A mesma infraestrutura está pronta para escalar para outros campos e permitir projetos de grande escala e crowdsourced que atualmente são difíceis de coordenar. Um exemplo clássico é a classificação de grupos simples finitos: um esforço de décadas distribuído entre muitos colaboradores, com inevitável complexidade em contabilidade, integração e confiança na completude. Com ferramentas modernas, imaginamos enfrentar desafios de escopo comparável: muitos colaboradores lidando com casos diversos, e sistemas automatizados unindo as peças. O campo torna-se um painel de progresso ao vivo que registra o que foi provado, o que permanece e exatamente quais dependências cada componente requer. Isso abre a possibilidade de uma forma muito mais rápida e envolvente de fazer matemática. Assista ao esboço de Tao no YouTube: