Lean for teaching university mathematics: current work and future research

Add to your list(s) Download to your calendar using vCal

• Paola Iannone (University of Edinburgh)
• Wednesday 11 June 2025, 09:15-10:15
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

BPRW03 - Big proof: formalizing mathematics at scale

It has become difficult to think about a future for mathematics research that does not include Interactive theorem provers (ITPs) and ITPs are entering the classroom everywhere. The list of courses using Lean, one such ITP ,  on the Lean community page includes – at the time of writing this abstract – 49 courses. These are both ‘transition to proof’ type courses and more advanced course for finalists and postgraduate students.   In this talk I will map  current (educational) research on the use of Lean for teaching and, in order to do so, I will first discuss some findings from educational studies on the impact of using Lean as part of ‘introduction to proof’ courses in first year university mathematics. I will particularly  focus on what research can tell us about the interaction between human (student) and tool (Lean). I will  then draw some conclusions on the affordances and drawbacks of using Lean  to support students’ transition to university mathematics and indicate some directions for future research.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.