Abstract. Yves Bertot, in his pedagogical wisdom, gives the following simple problem in his introduction to the Rocq Proof Assistant: “Is the product of two consecutive natural numbers even?” This simple problem is a classical exercise in elementary mathematics, but tackling it mobilizes all the growing cognitive faculties of the learner, from decomposing this informal mathematical statement into its components – from what it means for two natural numbers to be consecutive to the nature of even numbers – to formalizing these components, composing the results of these formalizations into a suitably quantified formal mathematical statement, and then proving this statement formally. The problem can be fruitfully generalized to investigating the divisibility properties of the product of three (or four, or five, … ) consecutive natural numbers. Overall, Yves Bertot’s simple problem gives rise to an engaging adventure of mathematical and computational discovery (as well as to one of self discovery), which the present article describes.

Olivier Danvy is interested in all aspects of programming languages, including programming.