Computer Assisted Theorem Proving for the Education

June 30, 2016, Stasbourg


The goal of this session is to bring together specialists of interactive and automatic theorem proving and specialists of mathematics education. This session was organized by Julien Narboux.


Tomas Recio (University of Cantabria)

Special session talk tomas estrasburgo.pdf

Title: "Computer assisted theorem proving for the education or Computer assisted education for theorem proving?”.

Abstract: The talk will be dual, in the sense of addressing the same issue from two different perspectives. One, in which the goals of mathematics education are a priori settled and computer assisted theorem proving is considered as a medium to achieve the given goals. Another one, where the goals of mathematics education should be reconsidered in view of the popularization of automated theorem proving features in dynamic geometry programs.

Benoit Rognier (

Edukera - strasbourg CATPE 2016.pdf

Title: "edukera : a point and click proof assistant for education".

Abstract: With edukera, students can now build mathematical proofs by selecting appropriate theorems among the list of authorized/available theorems. The presentation covers:

  • proof development interface (natural deduction style, scopes, backward/forward modes)
  • theory design for educational purposes
  • coq engine add-ons (paper management, term rewriting under lambdas)
  • student feedback (from experiment at UPMC university)

Corneliu Hoffman (University of Birmingham)

SpatchCoq: towards an accessible Coq interface for the working mathematician.

We present an interface to Coq that would allow easy access for a novice student/researcher into the world of Coq. This is still work in progress but the idea is twofold: 1. Create a collection of rather verbose Coq tactics that would be recognisable to a student/researcher that has no experience with proof assistants. 2. Cover Coq with an interface that would limit access to only those tactics in order to teach proof techniques.

As a byproduct the interface will also be able to generate more verbose Latex translation of the proofs with the final aim of mimicking natural language. Long term plans include interfacing with Computer Algebra systems in order to enhance the reach of computer assisted proofs.