Teaching Lean to undergrads

Stream: general

[Hunter Monroe]

@Kevin Buzzard what specifically is the call to action for universities considering acquainting undergraduate math majors with Lean--for instance, University of Maryland where both you and @Mario Carneiro spoke last week. Some options: (1) In the introduction to proof course that every math major must take at every university, the instructor could just refer students to the natural numbers game, without changing the course content. Instructors might want to track students' progress which would require accounts--is this a possibility? (I could help.) In any case, the game could benefit from a hall of fame, or its material could be added to codewars which has inadequate coverage of Lean. (2) The instructor could offer students the option of completing Lean exercises for each proof that is already taught in the existing curriculum (see for instance the existing UMD course https://www-math.umd.edu/undergraduate/departmental-course-pages/offered-courses/378-math-310-introduction-to-analysis.html). This would require the instructor or an assistant to get up to speed on Lean and create Lean files for each proof. Is there a cookbook for this and are there examples for instance at Imperial or CMU? (3) As a third option, the instructor could revise the syllabus in line with the CMU course as described in https://www.andrew.cmu.edu/user/avigad/Papers/learning_logic_and_proof.pdf and https://leanprover.github.io/logic_and_proof/, or make those supplementary textbooks. This seems like an excellent course--do CMU math majors have to take it? (4) Finally, enthusiasts could form a club like Xena.

Here are links to UMD recordings for you https://umd.zoom.us/rec/share/J0hZUClJC0mHMEWqc51WvA7muI_8Imf3Y7BxoiUNbcJ-Lt1GIlUjBq5uT3RGiHKU.h3c7Dc1TxUbvlVH- and and Mario https://umd.hosted.panopto.com/Panopto/Pages/Viewer.aspx?id=cba3dd82-1842-4b9f-a0a1-ad1601444ba4

[Patrick Massot]

Did you watch this panel discussion?

[Kevin Buzzard]

I figure that we teach maths students how to use computer algebra packages so why not teach them how to use computer proof systems? They're teaching them to computer scientists. Mathematicians might figure out cool things to do with them

[Oliver Nash]

I almost think it's a dereliction of duty _not_ to teach math undergrads computer proof systems.

[Patrick Massot]

We should only hire as postdocs people who worked in the real world. That really teaches proper respect for your boss :grinning:

[Matthew Ballard]

One aspect of introducing Lean into the mathematics curriculum that can be overlooked is the value it provides to non-math majors. In my course reviews, one student commented specifically that they would be able to add experience with formal verification to their CV. Inclusion of Lean can fly under the banner or integrative or experiential learning. Funding for curricular development along these lines is real possibility.