Coq/Rocq tutorial: Ssreflect tactics and the MathComp library
De Marie Kerjean
Creative telescoping for D-finite functions - Lecture 1
De Christoph Koutschan
Creative telescoping for D-finite functions - Lecture 2
De Christoph Koutschan
Apparaît dans la collection : 2014 - T2 - Semantics of proofs and certified mathematics
Thomas Hales (University of Pittsburgh): Formalizing the proof of the Kepler Conjecture