package coq-mathcomp-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.