The bedrock of mathematical activity is undoubtedly the concept of proof. Considering the abstract and conceptual nature of mathematical proofs, the act of proving is sometimes “thought to be the aspect of mathematical activity most resistant to the influence of technological change”. After a careful reading of “Proof Technology in Mathematics Research and Teaching”, however, one is convinced that the reality is quite different. In recent decades, development of tools such as automatic theorem provers has changed the work of mathematicians to the point of them questioning the very notion of mathematical demonstration. However, there is relatively little of this technological upheaval reflected in mathematics education.

This book is intended for specialists in mathematics education with an interest in computer science advances as well as for researchers in the field of automated reasoning with an interest in the pedagogical and didactic implications of their work. It provides a valuable contribution to mathematics education by initiating a process of in-depth reflection on the educational value of new technological tools such as automatic theorem provers and dynamic geometric environments. Considering the wide range of subjects covered, few people will read this book from cover to cover with an unfaltering enthusiasm. There is no doubt, though, that there is something here to satisfy everyone’s mathematical appetite.

The first chapter of the section titled “Automatic Theorem Provers” sheds light upon the reasons why the great advances made in automated reasoning have been slow to be reflected in the teaching of mathematics. The proofs produced by the automatic theorem provers are often deemed terse to the point of being unreadable. This explains why there are still very few mathematicians making widespread use of proof assistants. In order to mitigate the impact of the significant gap between the way humans express their mathematical thinking and the write-ups produced by the machine, the authors committed themselves to identify a possible source of this communication incompatibility. For humans, the raison d’être of a mathematical proof is not only to confirm the veracity of a statement. When a mathematician produces or consults a proof, he seeks above all an explanation; he seeks to base his understanding upon more elementary statements. Hence, clarity and readability are cardinal virtues. This is why the authors set themselves the objective of creating a program which would solve mathematical problems and which would present the solution using human-style prose.

The second chapter stands out through its profound foundational implications. By carrying out a detailed analysis of Cauchy’s Proof of Euler’s theorem, the authors demonstrate that it is not possible to translate this proof (procedural in nature) to “a sequence of formulae each of which is either an axiom or follows from earlier formulae by a rule of inference.” In doing so, the authors call into question one of the most prevalent assumptions in mathematics education. The “Theoretical Perspectives on Computer-Assisted Proving” section – by far the most heterogeneous – contains a reflection on didactical issues at the interface of mathematics and computer science, a deep analysis of the instrumental proofs, and a description of the means by which computers can enable students to prove results which would otherwise have been beyond them. Finally, a thorny question is tackled: to carry out a fruitful mathematical activity, do you need to have exceptional skills or, on the contrary, is the mathematician a craftsman whose skills only develop through apprenticeship and practice? The authors sought to find out by questioning illustrious witnesses such as Sir Isaac Newton, G. H. Hardy, and Terence Tao. An impression emerges from this chapter: if mathematics sometimes progresses following individual flashes of genius, the joke from the American golfer Arnold Palmer (“It’s a funny thing, the more I practice, the luckier I get.”) also seems to apply to mathematics.

The section “Suggestions for the Use of Proof Software in the Classroom” deals exclusively with geometry, a branch of mathematics which lends itself well to extensive use of interactive visualization technology. In the section called “Classroom Experience with Proof Software”, it is emphasized that to be profitable, learning mathematics using new technologies requires carefully planned lessons. Although geometric reasoning and manipulation once again occupy a prominent place, this section also contains a chapter on the teaching of Logic and Proof with an interactive theorem prover. The author sets out the course outline and the educational objectives of an undergraduate course which he co-developed and in which we focus on the synergistic effect of the simultaneous learning of the informal mathematical language, formal symbolic logic, and finally, the language of the Lean interactive theorem prover.

Frédéric Morneau-Guérin is a professor in the Department of Education at Université TÉLUQ. He holds a Ph.D. in abstract harmonic analysis.