SwissMAP Logo
Log in
  • About us
    • Organization
    • Professors
    • Senior Researchers
    • Postdocs
    • PhD Students
    • Alumni
  • News & Events
    • News
    • Events
    • Online Events
    • Videos
    • Newsletters
    • Press Coverage
    • Perspectives Journal
    • Interviews
  • Research
    • Basic Notions
    • Phase III Directions
    • Phases I & II Projects
    • Publications
    • SwissMAP Research Station
  • Awards, Visitors & Vacancies
    • Awards
    • Innovator Prize
    • Visitors
    • Vacancies
  • Outreach & Education
    • Masterclasses & Doctoral Schools
    • Mathscope
    • Maths Club
    • Athena Project
    • ETH Math Youth Academy
    • SPRING
    • Junior Euler Society
    • General Relativity for High School Students
    • Outreach Resources
    • Exhibitions
    • Previous Programs
    • Events in Outreach
    • News in Outreach
  • Equal Opportunities
    • Mentoring Program
    • Financial Support
    • SwissMAP Scholars
    • Events in Equal Opportunities
    • News in Equal Opportunities
  • Contact
    • Corporate Design
  • Basic Notions
  • Phase III Directions
  • Phases I & II Projects
  • Publications
  • SwissMAP Research Station

Teaching "Foundations of Mathematics" with the Lean Theorem Prover

Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara

13/1/25 Published in : arXiv:2501.03352

This study aims to observe if the theorem prover Lean positively influences students' understanding of mathematical proving. To this end, we perform a pilot study concerning freshmen students at the University of Zurich (UZH). While doing so, we apply certain teaching methods and gather data from the volunteer students enrolled in the "Foundations of Mathematics'' course. After eleven weeks of study covering some exercise questions implemented with Lean, we measure Lean students' performances in proving mathematical statements, compared to other students who are not engaged with Lean. For this measurement, we interview five Lean and four Non-Lean students and we analyze the scores of all students in the final exam. Finally, we check significance by performing a t-test for independent samples and the Mann-Whitney U-test.

Entire article

Phase I & II research project(s)

  • Field Theory
  • Geometry, Topology and Physics

Phase III direction(s)

  • From Field Theory to Geometry and Topology

3D Supergravity in the Batalin-Vilkovisky Formalism

Equivariant localization in Batalin-Vilkovisky formalism

  • Leading house

  • Co-leading house


The National Centres of Competence in Research (NCCRs) are a funding scheme of the Swiss National Science Foundation

© SwissMAP 2025 - All rights reserved