Nine Chapters of Analytic Number Theory in Isabelle/HOL.

DOI10.4230/LIPIcs.ITP.2019.16OpenAlexW2978388704MaRDI QIDQ5875424

Manuel Eberl

Publication date: 3 February 2023

Full work available at URL: https://doi.org/10.4230/LIPIcs.ITP.2019.16

zbMATH Keywords

theorem provingprime number theoremDirichlet seriesarithmetical functionnumber theoryDirichlet's theoremIsabelleanalytic number theory

Mathematics Subject Classification ID

Related Items

What is the point of computers? A question for pure mathematicians ⋮ A formalization of Dedekind domains and class groups of global fields

Uses Software

• Locales
• Archive Formal Proofs

Cites Work

• Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL
• Locales: a module system for mathematical theories
• Formalizing an analytic proof of the prime number theorem
• Proving Pearl: Knuth’s Algorithm for Prime Numbers
• Euler and the Zeta Function
• Analytic Number Theory
• Verified Real Asymptotics in Isabelle/HOL
• A formally verified proof of the prime number theorem
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• A simple derivation of \(\zeta(1-K)=-B_K/K\).
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item