Skip to content

Accompanying files for the paper "Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis"

Notifications You must be signed in to change notification settings

jnarboux/PA_a_priori_analysis

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

21 Commits
 
 
 
 
 
 
 
 

Repository files navigation

Proof assistant for undergraduate mathematics education: elements of a priori analysis

The repositoty contains accompanying files for the paper "Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis"

This paper presents an a-priori analysis of the use of five different interactive proof assistants for education, based on the resolution of a typical undergraduate exercise on abstract functions. It proposes to analyse these tools according to three main categories of aspects: language and interaction mode, automation and user assistance, and proof structure and visualisation. We argue that this analysis may help formulate and clarify further research questions on the possible impact of such tools on the development of reasoning and proving skills.

Case study

For formalize the following two exercises using several proof assistants.

Given f:A→B and C⊆A, show that C⊆f^(-1) (f(C)).

Given f:A→B and C⊆A, show that if f is injective then f^(-1) (f(C))⊆C.

List of proof assistants we experimented with:

Screenshots

DEAduction

Isabelle/HOL

The proof formalized without using automation using the Isar language:

ISABELLE_PROOF

Edukera

The popup window when clicking on a definition:

Screenshot Edukera Popup

During the proof:

Screenshot Edukera (unfinished proof)

An option is also available to display the proof tree:

edukera proof tree

Lurch

Lurch screenshot (properties and direct implication, with validation)

Lurch screenshot (converse, with injectivity, with validation)

Videos

Authors

  • Evmorfia Iro Bartzia
  • Antoine Meyer
  • Julien Narboux

About

Accompanying files for the paper "Proof assistants for undergraduate mathematics and computer science education: elements of a priori analysis"

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published