Missing website pages

Stream: general

[Yury G. Kudryashov]

I suggest that we add (at least) two more pages to the community website:

1. A webpage listing past and future Lean-related events with brief description (target audience, dates, venue, website, application deadline, is it lean-specific or not). Most of them are announced somewhere in this chat but this is not the best interface.
2. A webpage listing university courses that use Lean in one way or another with brief descriptions.

I can try to write some drafts tonight or tomorrow but these drafts will look better if you reply here with links to events and courses.

[Kevin Buzzard]

Event: ICERM is here https://icerm.brown.edu/topical_workshops/tw-22-lean/ , it's July 2022, applications are open.

Hot gossip: I just heard today that my Hausdorff Research Institute (Bonn) proposal "Prospects of Formal Mathematics" will be running May to August 2024. More details forthcoming.

Courses:

My formalising mathematics 2021 course has repo here https://github.com/ImperialCollegeLondon/formalising-mathematics and there are links to 9 blog posts covering an introduction and the 8 workshops in the repo.

My formalising mathematics 2022 course is currently in progress; repo is here https://github.com/ImperialCollegeLondon/formalising-mathematics-2022 and course notes are here https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/ and youtube playlist is here https://www.youtube.com/playlist?list=PLVZep5wTamMmRPvCLO4WVpCwkTi1F6OyF (all currently increasing in size; course finishes end of March)

[Yury G. Kudryashov]

Can you share some information about the students who actually attended your courses (publicly or privately): how many tried? How many got credit for the course? Were they all math majors or students with other majors (cs?) attended too?

[Yury G. Kudryashov]

I want to suggest a course with formalized proofs and success stories from other universities can help.

[Yury G. Kudryashov]

Other events I know about: ITP, past lean together and lftcm meetings

[Yury G. Kudryashov]

What did I miss?

[Yury G. Kudryashov]

I also found https://popl22.sigplan.org/series/CPP

[Jeremy Avigad]

I have taught courses on interactive theorem proving a few times at Carnegie Mellon. The last time was in the fall of 2019. I had 19 students, 11 grad and 8 undergrad. While Jesse Han was taking it, he and Floris van Doorn formalized the proof of the independence of the continuum hypothesis. Needless to say, he passed.

I'll be teaching another course next fall, this time targeted specifically at undergraduate math majors.

[Jeremy Avigad]

Rob Lewis taught one last semester, in the CS department at Brown: https://cs.brown.edu/courses/cs1951x/.

[Matthew Ballard]

I taught our Transition to Advanced Mathematics here at USC in Fall 2020. This was a standard intro to proofing course for math majors. I followed Jeremy’s lead pretty strongly using Logic and Proof. The course was 1/3 homework, 1/3 presentations, 1/3 final project. The homework had a significant Lean component and most people elected to beat the NNG for their final project. There were 15 students and I found the Lean feedback overall very positive.

Alas there is no outward facing material. It is all stuck behind MS Teams.

Next fall will be a repeat of this course. I plan on getting auto-grading going properly and running it through GitHub classroom.

In the spring, we are planning to run an honors course for undergraduates modeled on the Vrije course

[Patrick Massot]

My course is called "Logic and computer assisted proofs". It is attended by 50 to 60 students, first year undergrad with math/CS double major. Lecture notes and exercises can be found at https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/ (MDD154 is the course code). In the exam students prove lemmas in Lean and then write the proof on paper. The main math content is proofs of properties of sequences of real number. There is very little pure logic.

[Kevin Buzzard]

My two courses:

The 2021 course ran on Discord and was part of the EPSRC Taught Course Centre program. It was attended by around 15 PhD students none of whom knew anything about Lean. Two of them needed a pass/fail grade so I made them write some code and then gave them a pass.

The 2022 course is for final year undergrads and is part of our official undergraduate curriculum. It is examined by three projects; 21 students handed in projects for the first deadline last Friday and I strongly suspect I'll get 21 submissions for the other two (because once you've submitted a project you've committed to taking the class). Of the 21 students 20 are maths student and one is from the computing department (teaching is heavily department-based in the UK; you do not "major in X", you come to university with "I do X" stamped on your forehead and then only do classes from department X; the computing person had to explicitly ask for the rules to be bent and I had to argue for them).

[Kevin Buzzard]

PS @Matthew Ballard all of my teaching material is stuck behind blackboard (our VLE). I don't know who this Xena guy is leaking it all to YouTube without asking the department's permission

[Rob Lewis]

I'm very much in favor of adding these pages to the website

[Rob Lewis]

Jeremy Avigad said:

Rob Lewis taught one last semester, in the CS department at Brown: https://cs.brown.edu/courses/cs1951x/.

This course was also adapted from Jasmin's Logical Verification course at the VU. Taught to a mostly CS audience (with quite a few math-CS double majors), ranging from second-year undergrads to PhD students, 28 total

[Rob Lewis]

10 homework assignments and a required final project. The course was an experiment and I was really happy with how it turned out -- the final projects were, on the whole, far beyond what I was expecting to see

[Kevin Buzzard]

The same happened for my course. Three projects; I spent the weekend marking the first one. There were people like Jason KY who just submitted his PR of Egorov's theorem and a couple of other Lean experts, but there were some people who had come from 0 to proving the Bolzano-Weierstrass theorem or Cauchy <-> convergent in 3 weeks, and others just did totally random things like defined Dedekind cuts and proved a ton of stuff about them, or proved completeness and soundness for first order logic (that was a computing student) or some graph theory etc. It's interesting seeing what these people come up with.

[Matthew Ballard]

Unfortunately, I recorded my lectures in MS Teams and they got uploaded to the local instance of MS Stream so everything is trapped within Office 365. I think it was more a function of lack of forethought.

VLE = LMS? We have Blackboard here also. There is an API for interacting with it LTI. Obviously some should build a client in Lean 4 :)

The course description for the previous was

Rigor of mathematical thinking and proof writing via logic, sets, and functions. Intended to bridge the gap between lower-level (computational-based) and upper-level (proof-based) mathematics courses.

We only expected the students to have passed calculus 2 and in practice the majority were freshmen or sophomores.

[Rob Lewis]

I opened https://github.com/leanprover-community/leanprover-community.github.io/pull/254 for one of these ideas -- will leave the courses page for later!

[Rob Lewis]

I'm not sure if it makes sense or not to list events like CPP and ITP. These aren't Lean-specific and typically only have a few Lean papers at them. On the other hand, they could be of interest to people who care about other events on the list.

[Yury G. Kudryashov]

There are different types of potential readers:

1. People who want to know more about Lean. They probably don't want to see CPP and ITP on this webpage.
2. People like me who came to Lean from traditional math and don't know how to turn their work into published papers. We should have a page that suggests "prepare a paper for ITP" as one of the possibilities.

[Kevin Buzzard]

There was a question on the proof assistants SE of the form "I'm a mathematician; I know some tactics but have no idea how to make my way around the API" and it would be good if we had some kind of place to point these people. NNG makes an object and its API from scratch without using anything from mathlib other than tactics. The moment you want to deal with objects defined in mathlib you have to pick up some different skills. I spent the first month of my code t teaching tactics and using rcases to take terms apart and talking about definitional equality, but now in the second month I need to start teaching these people how to use library API and this is a different kind of problem to figuring out the difference between apply and rw.

[Rob Lewis]

Yury G. Kudryashov said:

There are different types of potential readers:

1. People who want to know more about Lean. They probably don't want to see CPP and ITP on this webpage.
2. People like me who came to Lean from traditional math and don't know how to turn their work into published papers. We should have a page that suggests "prepare a paper for ITP" as one of the possibilities.

I added some links to the draft, but then had two thoughts:

• The list should be generated from a yaml file, like other pages on the website, so we don't have to manually move things from "future" to "past"
• Would tagging events ("CS conference", "workshop", "tutorial", ...) help? And what should the categories be?

[Rob Lewis]

image.png

[Rob Lewis]

Feel free to add to the PR