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
Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau): Digitizing the Group Theory of the Odd Order Theorem