Undergraduate summer project

Stream: new members

[Lior Silberman]

Hello. I have two summer students who will work with me on formalizing some mathematics in Lean. Essentially this is a summer project in research infrastructure rather than in research. If this is successful I will think about doing this on a more regular basis.
Q1: which tutorials are recommended for students?
Q2: I will discuss the mathematics to be encoded based on what the students know and what is of interest/use to me -- but is there a way to solicit suggestions from the community?
Thanks, Lior (UBC)

(if this is the wrong part of the forum for this let me know)

[Kevin Buzzard]

Natural number game to start them off, then Mathematics In Lean

[Lior Silberman]

Thanks, Kevin!