Terence Tao, inaugural Veritas Fellow — autoformalizing number theory | Math, Inc.

Organizing Analytic Number Theory

• 💡 The project aims to organize the complex literature of analytic number theory, which is a vast, interconnected network of estimates.
• 🎯 Estimates are categorized into primary (e.g., zero-free regions for the zeta function from computations), secondary (converting primary to things like counting primes in intervals), and tertiary (applications to problems like sums of three primes).

Addressing Literature Mismatches

• ⚠️ A key problem is the mismatch between updated computations and older papers, where new estimates are not integrated, leading to outdated results.
• 🧩 This prevents understanding the updated implications of new inputs on existing applications and estimates downstream.

A Modular Formalization Approach

• 🚀 The solution involves formalizing key papers and automatically abstracting them to create a living, modular network of implications.
• ✅ This modularity allows researchers to add or subtract literature, test the impact of specific papers, and organize knowledge at a level above single publications.

AI and Formalization as Connecting Glue

• 🧠 AI and formalization are envisioned as the "connecting glue" to integrate different papers and literature, especially those with slightly incompatible hypotheses.
• 🔬 While number theory is a strong test case due to its well-defined structure, this paradigm is designed to scale to other fields of mathematics, such as Partial Differential Equations (PDEs).

Crowdsourcing Large-Scale Math Projects

• 🌱 A future vision is to crowdsource massive mathematical projects, like the classification of finite simple groups, which previously took decades and required single experts.
• 📈 Automated technology could track progress (e.g., "67% of cases covered"), making complex mathematical endeavors more engaging and significantly faster.