Formalizing an analytic proof of the prime number theorem

DOI10.1007/s10817-009-9145-6zbMath1185.68624OpenAlexW1984801909WikidataQ56059244 ScholiaQ56059244MaRDI QIDQ2655322

Yanyan Li

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9145-6

zbMATH Keywords

prime number theoremanalytic proofcomputer formalization

Mathematics Subject Classification ID

Related Items (15)

HOL Light: An Overview ⋮ Computational logic: its origins and applications ⋮ Unnamed Item ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ A formalised theorem in the partition calculus ⋮ Formalising Mathematics in Simple Type Theory ⋮ What is the point of computers? A question for pure mathematicians ⋮ Proof pearl: Bounding least common multiples with triangles ⋮ Proof Verification Technology and Elementary Physics ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ Pollack-inconsistency ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A formal proof of Pick's Theorem ⋮ A Formal Proof of Cauchy’s Residue Theorem

Uses Software

• ML
• HOL
• HOL Light

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• The free will theorem
• Obvious inferences
• PRIMES is in P
• Edinburgh LCF. A mechanized logic of computation
• Primality Proving with Elliptic Curves
• Towards Self-verification of HOL Light
• Newman's Short Proof of the Prime Number Theorem
• Analytic Number Theory
• A Fascinating Country in the World of Computing
• Theorem Proving in Higher Order Logics

This page was built for publication: Formalizing an analytic proof of the prime number theorem