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.

Mid-term meeting

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

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

This task focusses on modifying the elaboration phase of the proof engine so that structures (like ring of field structures) or theorems (like the theorem stating that some operation is associative) can be inferred automatically from the working context. Researchers involved in this task will be holding a meeting on this topic the week of December, 2nd, 2024. Dedicated page.

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

First example and Second example used by D. Hamelin at a talk given at ThEdu 2024.

How to update this web-site

Instructions are available here.