# 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
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.