LiberAbaci

Computer proof tools have gained recognition in the production of reliable software and the verification of complex mathematical proofs. The objective of this challenge is to understand how Coq can facilitate mathematics education, especially in the first university years. Research question for this project are: how should the foundations of type theory be adapted for this purpose?  How should knowledge be structured?  How can one close the gap between the language for computer treatment and the usual language of mathematics?  How to take advantage of automation for educative purposes?  How to provide to all students a working environment that is conducive to learning?  How to gather enough teaching material to attract educators and students? All these questions should be studied in collaboration with mathematics educators.