New Technologies in Mathematics Seminar

Speaker: Xinjie He, UCLA

Title: The IEANTN Project: Automation and Mathematical Understanding

Abstract: Explicit analytic number theory combines conceptual arguments with extensive bookkeeping and numerical computation, often drawing on long chains of results across many papers. The Integrated Explicit Analytic Number Theory Network (IEANTN) aims to organize this literature into a living network whose dependencies and supporting evidence are explicit.

In this talk, I will discuss how we redesigned IEANTN from its 1.0 version, which put everything in a single Lean repository that was hard to maintain and rebuild as auto-formalization produces increasingly large proofs, to its current 2.0 version, which solves this problem by separating readable mathematical statements from verified proofs and recording different levels of justification.

Finally, I will discuss what we hope to automate and what we want to understand ourselves. By organizing the literature into a network, we hope to make the mathematical ideas and relationships easier to see, and leave the detailed bookkeeping to machines.