LiberAbaci

Teaching mathematics with the help of Coq

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.

Events and notable results

Kickoff meeting

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.

Tasks

Task 1 : Collaborating with teachers

We are working on establishing contacts with mathematics teachers and researchers in didactics. Dedicated page

Task 2 : Foundations of type theory

Task 3 : Structures, inference, and hierarchies

Task 4 : extensible Notations and surface langage

This task focusses on experimenting new notation mechanisms and new structures for the proof language, to get as close as possible to the usual notation in a mathematics curriculum. Dedicated page

Task 5 : Automation

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

Task 6 : Interactive development environments

Task 7 : Creating ressources on specific domains

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 page

How to update this web-site

Instructions are available here.