Toward the use of a proof assistant to teach mathematics

International audienceProof is a crucial aspect of mathematics and must have a prominent role in the education. Dynamic Geometry Software (D.G.S.) and Computer Algebra Software (C.A.S) are widely used in a pedagogical context. These tools are used to explore, visualize, calculate, find counter examples, conjectures, or check facts, but most of them can not be used to build a proof in itself. But there are software whose sole purpose is to help the user produce proofs : the proof assistants. We believe that proof assistants are now mature enough to be adapted to the education. After giving a quick overview of what a proof assistant is, we will discuss the possible advantages of using it in the education. Finally we report on the ongoing work to ease the use of a proof assistant in the classroom