Apery

This project contains a formal proof that the real number ζ(3), also known as Apéry's constant, is irrational. It follows roughly Apéry's original sketch of a proof. However, the recurrence relations constituting the crux of the proof have been guessed by a computer algebra program (in this case in Maple/Algolib). These relations are formally checked a posteriori, so that Coq's kernel remains the sole trusted code base.

Meta

• Author(s):
  • Frédéric Chyzak (initial)
  • Assia Mahboubi (initial)
  • Thomas Sibut-Pinote (initial)
• Coq-community maintainer(s):
  • Assia Mahboubi (@amahboubi)
  • Kazuhiko Sakaguchi (@pi8027)
• License: CeCILL-C
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • MathComp ssreflect 2.0 or later
  • MathComp algebra
  • MathComp field
  • CoqEAL 2.0.0 or later
  • MathComp real closed fields 2.0.0 or later
  • MathComp bigenough 1.0.1 or later
  • Mczify 1.5.0 or later
  • Algebra Tactics 1.2.0 or later
• Coq namespace: mathcomp.apery
• Related publication(s):
  • A Formal Proof of the Irrationality of ζ(3)
  • A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) doi:10.1007/978-3-319-08970-6_11
  • Reflexive Tactics for Algebra, Revisited doi:10.4230/LIPIcs.ITP.2022.29

Building and installation instructions

The easiest way to install the latest released version of Apery is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-apery

To instead build and install manually, do:

git clone https://github.com/coq-community/apery.git
cd apery
make   # or make -j <number-of-cores-on-your-machine> 
make install