Co-located event

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.

Organization

This informal session will be organized by Julien Narboux.

Talks

Tomas Recio (University of Cantabria)

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.com)

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)

Confirmed participants

• Vincent Pavan (University of Provence)