A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)

DOI10.1007/978-3-319-08970-6_11zbMath1416.68155OpenAlexW2100238579MaRDI QIDQ2879250

Thomas Sibut-Pinote, Enrico Tassi, Assia Mahboubi, Frédéric Chyzak

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08970-6_11

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) (zeta (s)) and (L(s, chi)) (11M06) Irrationality; linear independence over a field (11J72)

Related Items (10)

Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec ⋮ Multiple binomial sums ⋮ Some open problems related to creative telescoping ⋮ Unnamed Item ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ What is the point of computers? A question for pure mathematicians ⋮ Proof pearl: Bounding least common multiples with triangles ⋮ Creative telescoping on multiple sums ⋮ Verified interactive computation of definite integrals ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• Coq
• Maple
• Algolib
• HOL Light

This page was built for publication: A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)