Mathematical skills > Assessment of proof

Question 50
What can automated theorem provers (e.g. LEAN) offer to the e-assessment of proof comprehension?

• Paola Iannone
• Ben Davies

Automated theorem provers have been around for many years and recently they have been used by those mathematicians who are interested in automated checking of proofs. To the best of my knowledge, although not used in the UK, they are used in some countries in some pure math modules (e.g. Germany and Canada) for teaching. Using those could help address some interesting gaps: gap between what mathematicians use in research and what they use for teaching, lack of programming for pure math modules. However we know every little about their potential as teaching tools.

What motivates this question?

It would allow students to get programming experience in pure math but above all it would interest to mathematicians (who may be using those tools in research). This may mean that the use of this automated provers may remain as a feature of teaching and may not disappear after an initial trial. (I am thinking about the case of ISETL - perfectly developed programming language for students to help them with proof, copying with all documents etc - nobody uses it anymore). Moreover the features of these programming tools could address some of the known problems that students have with proof

What might an answer look like?

Some preliminary work on the effect of using LEAN on proof writing and proof production already exists, but it would be very interesting to do a more structured study. In the example I mention above LEAN was not part of instruction for all students so it would be interesting to have a study on a module where LEAN is part of the instruction. An answer may highlight proof writing behaviour which can be traced back to the experience of programming - this has been done for other programming languages used for teaching so we may look at such studies for designing one

Related questions

• Students creating proofs in a formal language could be one approach relevant to Q49: How can the assessment of proof be automated?

• We don’t really know much about what students think about these automated provers, related to Q17: What are students’ views on e-assessment, and what are their expectations from automated feedback?

• Use of automated provers is one case that could be considered in Q13: How do students interact with an e-assessment system?

References

Avigad, J. (2019). Learning logic and proof with an interactive theorem prover. In Hanna, G., Reid, D. and de Villiers, M. (Eds,). Proof Technology in Mathematics Research and Teaching: Mathematics Education in the Digital Era (pp. 277-290). Springer.