A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
F. Chyzak,A. Mahboubi,T. Sibut-Pinote,Enrico Tassi
2014 · DOI: 10.1007/978-3-319-08970-6_11
International Conference on Interactive Theorem Proving · 28 Citations
TLDR
The formal verification of an irrationality proof of ζ(3), the evaluation of the Riemann zeta function, using the Coq proof assistant is described, complete up to a weak corollary of the Prime Number Theorem.