Teaching Divisibility and Binomials with Coq

TL;DR

This paper presents Coq-based worksheets designed to teach divisibility and binomials, including exercises and pedagogical strategies, supported by an initial student experiment, aiming to enhance early mathematical education.

Contribution

It introduces a set of Coq worksheets with exercises and pedagogical guidance for teaching divisibility and binomials, including experimental validation.

Findings

Worksheets are freely available and adaptable.

Additional Coq lemmas and tactics are necessary.

Preliminary student experiment conducted.

Abstract

The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices, the numerous exercises we developed and a small experiment we conducted on two students. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.