LiberAbaci is a collaborative project aiming at improving the usability of the interactive proof system Coq for an audience of students in mathematics in the first years of higher education.
The kickoff meeting happend on September 20, 2022 at Inria in Paris. The program of this meeting gives access to the various presentations given on that day.
We will hold a meeting on the whole progress in each task on October 17-18, 2024. The program of this meeting will be described in the following page
This tasks explores which tactics are the best suited to help the students progress in their comprehension of mathematics (which is not the same as performing proofs in their place).
On February 28, 2024, there was a meeting with the developers of Coq waterproof, where the question of automation was raised as one of the main points. Dedicated page for this meeting
The objective is to provide a collection of libraries motivated by teaching requirements, for instance in algebra, calculus (for instance Lebesgue integral), arithmetic (for instance divisibility).
There was a video conference on the topic on December 11, 2023.
Dedicated pageFirst example and Second example used by D. Hamelin at a talk given at ThEdu 2024.
Instructions are available here.