result of my lean mentorship program: 3 out of 16

Stream: Lean for teaching

[Bulhwi Cha]

The mentorship program I mentioned in the Lean Zulip chat started on September 9 and ended on October 25. There were sixteen applicants, and I chose all of them as my mentees. Our initial goal was to finish reading “Theorem Proving in Lean 4” while translating the Natural Number Game (NNG) into Korean.

It turned out I was overly ambitious. I took too much time to record videos of myself reading the textbook in Korean, create an additional quiz, review my mentees’ solutions to the questions in the quiz, and organize meetings with my mentees. Consequently, I could only cover the first three chapters of the book. As for NNG, I’m currently translating Tutorial World.

Unfortunately, nine mentees quit my mentorship program, seven of whom didn’t even solve any questions in my quiz for Chapter 2. Among the rest of my mentees, only three solved the quiz and the exercises in Chapter 3. Two other mentees managed to solve some of the questions in my quiz.

After my mentorship program, the three mentees who completed all the homework agreed to continue learning to use Lean under my guidance. They are all women, consisting of an undergraduate, a graduate, and a software developer. Although they are all programmers, none had read textbooks solely on formal logic before they applied for the mentorship program.

It appears that proof assistants are too complicated for most programmers, but some can have a good grasp of them. I wonder if the same is true of mathematicians.

[Bulhwi Cha]

I shared this post on the r/math subreddit, and someone gave the following comment:

kr1staps said:

It appears that proof assistants are too complicated for most programmers, but some can have a good grasp of them. I wonder if the same is true of mathematicians.

Given your extremely small sample size, and possible confounding variables, I don't think it's fair or logical to draw such broad conclusions. Especially since, by your own admission, the project was "overly ambitious". By publicly stating these conclusions, I think you're doing a disservice to the Lean community (which you seem to be a part of?) by giving the (unjustified impression) that it is "too complicated" for "most" programmers.

In fact, before Kevin Buzzard got involved, the majority of people who seemed to have any serious interest in (and the people who actually developed) Lean, were programmers. Speaking of Dr. Buzzard, who appears not infrequently in this sub, he has guided many undergrads in Lean projects who have had minimal programming or mathematical training. He's far from the only one either, there are quite a few people in the Zulip community that have had success teaching Lean to people at all levels, such as Adam Topaz and Heather Macbeth, just to name a few.

In recent years, there have been many successful summer schools and workshops on other proof assistants for undergrad, namely Coq and Agda.

[Freddie Nash]

My 2cent as a software engineer, CS educator, and recently trying-to-learn Lean programmer who has always been around coders (rather than mathematicians): it took me a couple of years to get into proof-assistants: number 1 problem was that I had no use for them, so I had no idea what they could do for me, and so I had no motivation to learn any particular language. I made a serious but failed attempt at learning Agda because I had a PhD colleague doing the same: I had no idea what was going on or why people were so excited about applying reflexivity (which of course I totally get now). The F* tutorial, however, changed my life, even though I hardly understood any of it on the first read: it was pitched to me as a programmer, and didn't even mention reflexivity until chapter 7 or something. It would have been even more confusing without a reasonable background in an ML like language (F#), which many programmers will not have. When I decided to learn Lean, this too I imagine I could only achieve on my own in a sensible time-frame because so much is the same as F*, the only glaring difference being exactly the reason I wanted to learn Lean: there's no SMT.

As someone who works with undergraduates a lot, I'd be very surprised if you couldn't teach a second-year CS undergraduate in an OK institution to write simple programs and proofs in Lean in 1 semester. I'd also expect about 5% of them to love the course and be doing the NNG and every other tutorial they can find in their free time, and 80% to just want it to be over: programmers are a seriously heterogenous group.

So the problems for programmers I can imagine:

• Programmers and programming languages are really diverse: ML/Haskell are good starting places to learn a language like Lean, but Java/C/Python are not: relevant features of 'functional' programming are considered very different already from what the majority of programmers are using for work, and translation from iterative to recursive implementations is a skill that has to be practiced
• It takes a while to see the benefits of a proof assistant - heck, there are programmers who don't see the benefit of a sensible type system _at all_, so good luck getting through to them - so I imagine its easy to lose people if something is optional: it will take weeks for it to click, and if they are allowed to drop-out before then I think it'll be hard to keep too many: on the other hand, I gave a 1-hour demo of F* at the company I work for, and at least 2 of the audience members were actively engaging
• Even when you can see the benefits, they're just not applicable to the sort of projects people actually do: if you're learning C# and want to make websites, there is a very obvious direction to move in. If you're learning Lean because someone said it was cool... what are you meant to do next? The engineering problems tools like F* are trying to solve are _hard_ (at least, they seem that way to me): it's not the sort of thing you decide to do one day for fun (and then devote a whole year to), or that's going to significantly broaden your job prospects.
• Most programmers don't know any formal logic: I was taught propositional logic in the first year of my computer science degree, and all the rest of the maths was calculus, linear algebra, complexity analysis, and differential equations, none of which helped when first learning a proof assistant. I'd completely forgotten propositional logic by the time I started my PhD: I basically learned it entirely again from this page on F*: https://github.com/FStarLang/FStar/wiki/Sugar-for-manipulating-connectives-in-classical-logic - I never saw any connection between the rigour of the proofs we were constructing in propositional logic and other maths
• ... probably because most programmers probably just can't do maths in a rigorous way: everybody glosses over division by zero, and we make large jumps in proofs without having any idea which words would be needed to fill in the gaps (I'd long forgotten what transitivity meant before I started working with total orders in Fstar, and now of course it's second nature because I have to name my lemmas): in a way, though, this is an easier problem than in programming: if I want to know how to open a file in Java because I've not touched it in 10 years, I had to google that: if I want to know if I can assume 2 > 1 in lean, I just type exact?, but I only found that by chance in this chat: it wasn't in the tutorials. Tools like Loogle are fantastic. Tools like simp make me sad. Proof by induction has to be second nature in Fstar/lean, but I feel I never understood it until I saw a decreases clause in Fstar and then everything clicked ("it's just termination checking!"): your average programmer won't have a clue about this.

Personally, I wish I'd had proof-assistants thrown at me repeatedly during my CS degree: I am so much happier with maths now that I have a tool for objectively checking things: any exam paper question that involved writing a proof always has problems with "which lemmas am I meant to know? is this jump too big? do I care about this singularity? can I just invoke the pigeon-hole-principle and move on with my life?": what was meant to be concrete and rigorous always felt wishy washy and open to interpretation: compare this with a (modern) compiled programming language, where "write a function with this API" is instantly checkable, and you can't argue with the outputs when run (or at least, any _programmer_ can agree when things start to get iffy (shared state, IO, randomness etc.)). It took me a long time and a lot of hard work to get to where I am (and I'm sure I'm still only scratching the surface), and I reckon I could have skipped a couple of years of that with tuition that was tailored to me, but again, programmers are heterogenous bunch so what would work for me wouldn't work for 80% of students around me.

Things that I found relatively useful early on, that maybe could be leaned on more:

• Calculational proofs: these look like the proofs I used to try to do on paper, and don't hide much: steps are completely obvious without knowing how to use the tooling effectively (these days I hardly use them because it takes too long, but they were invaluable for getting a feel for what I could do (what steps were legal))
• Lists were way more exciting than natural numbers for me as a programmer: you can write programs that do useful stuff with lists quite quickly, but who wants to have to use the Peano natural numbers for anything in the real world? When I demo F* to people (programmers), I always use lists as the first inductive type (F* has the SMT to help with nats, so less to be learned from them anyway). Exercises like quick-sort were great.
• VS Code based tooling: most programmers are not using emacs, and I do not want to be learning how to use yet-another text editor if I can reasonably avoid it
• F*/Lean syntax is much closer to heavily used programming languages than, say, Coq or Agda, so less of a burden up-front on that

Well that went a bit rambly: not meant to be any conclusion in there, but if there is one, it's that there are a lot of programmers and they're all different and I think you need to speak their language if you want to get through to those who are not already enthused with the idea. I certainly don't think proof assistants are "too complicated" (how many mathematicians can pick up an RDBMs/game engine/anything else programmers do day-in-day-out in a few weeks with essentially no background in programming?), but I absolutely think there is a big hurdle to be jumped, and I think Lean is doing a much much much better job at being accessible than the other familiar proof assistants.