Teaching with Verbose Lean

Stream: Lean for teaching

[Siddhartha Gadgil]

We will be having a 1 credit lab course Proofs Lab with Lean at the Indian Institute of Science, Bangalore. I had a few questions about the design: especially for @Patrick Massot but anyone else with experience with Verbose Lean (and also the Lean server).

• I was planning to use the exercises of proofs_with_lean. However, I see that the first 6 (and even the last two) are about the language and logic. How many weeks are these intended to take?
• Beyond this, a verbose version of selections from Glimpses of Lean seems a good source. Has anyone made/used such a source.
• To avoid installation issues for students, I was planning to run on our LAN an instance of lean4web with the relevant exercises added as "Examples". Any tips regarding this are welcome @Jon Eugster

[Snir Broshi]

Personally I'd take installation issues over lean4web any day, it's great for trying stuff out but the client-server architecture just makes it super slow, and it disconnects when switching tabs for a second.
LAN might make it a bit faster, but still the VSCode experience is pretty smooth IMO. I think VSCode wins if the goal is reducing issues.

[Patrick Massot]

I see I never translated the end of my course, it should not stop at file 10. I’ll try to find time for this soon (please remind me to do this if I forget).

[Patrick Massot]

The first few files are very quick. For instance the first three files are covered in the first two hours. Student slow down a lot when real mathematical content appears.

[Patrick Massot]

That being said, you could also try to remove even more logic if you really don’t want to discuss logic. You can simply say the main tactic is Since A and B we obtain D, with less or more facts before the conclusion, and maybe with the variationwe conclude that D at the end. Without discussing any logic rule, you can say there are two Since rules. First A and B must individually follow from at most one local assumption. Then D must follow from A and B and from lemmas that were registered for automatic use.

[Patrick Massot]

And I agree that being able to use Lean directly is much more robust than a lean4web server. However you may be able to setup some GitPod-like server where students can use Lean, and it may be an intermediate solution.

[Patrick Massot]

One last thing: I’m slowly updating Verbose Lean to catch up on recent Lean. I’m currently at 4.24 if I recall correctly. One good thing about reaching 4.26 is access to advanced logging information if you want information about what students do. Then I plan to use more automatic naming for newly obtained information because the Verbose Lean style I use (the one you see in proofs with Lean) never refers to those names and students very often forget to provide them.

[Patrick Massot]

I also need to experiment to see whether using grind internally can speed up Verbose Lean (which can be a bit slow in proofs with a lot of automation).

[Siddhartha Gadgil]

Thanks a lot @Patrick Massot
I am happy doing some logic so students use it correctly in proofs - maybe two sessions or so. My concern was that if each file was a session most of the course would be logic. But as the files are quick this is perfect.

I will wait for a newer version before getting my setup. I will probably try a hybrid solution - have a server for those who have installation issues (or just laptops with too little RAM) but encourage local installation (and do this on lab machines).

[Jon Eugster]

Fot a semester long course, I would probably do local installations, too. I've been part of 2-4h hour workshops done purely in the webeditor, which worked fine. It doesn't really support handling multiple files and saving progress locally though. Having a git repo with the exercsises to pull sounds like it would be a much cleaner experience. And I've got the impression that the point-and-click installation through VSCode has improved much over the last years,making the installation easier on Windows.

Regardless if you want to setup a local server. I've bumped Lean and most NPM-dependencies on this branch:

https://github.com/leanprover-community/lean4web/pull/76

I haven't merged it yet because there was a failing test (about Ctrl-click for docs) and I ran out of time fixing it. It might be worth a shot working from that branch if you're trying the installation right now, before it gets merged.

[Siddhartha Gadgil]

Thanks @Jon Eugster
It is likely that we will have the course in a lab and a student has volunteered to install Lean etc on all the machines. So that should take care of the main use.

I will still try to have a server though for students who may want to work at other times from laptops with too little RAM. The course starts in January, so I will wait a couple of weeks for merger before setting up.

[Michael Rothgang]

My understanding is that two months ago, having a notebook with 8GB of RAM is the bare minimum you need (and you'd have to be careful; import Mathlib could make your computer run out of memory). If there are problem, tell your students to open fewer tabs at the same time.

This situation has recently improved a bit: the module system work reduces this a lot (you need to use the module system in the course repository for this to apply), recent fixes to Lean core also help. (Not sure if these are released already, but the next stable version should surely have them.)

[Alex Kontorovich]

If you don't want to do a local install (and want to do real analysis), another option is the Real Analysis Game... https://adam.math.hhu.de/#/g/AlexKontorovich/RealAnalysisGame

[Patrick Massot]

This is really a completely different aim. The aim of Verbose Lean is to train students to read and write traditional proofs on paper, not to learn Lean.

[Siddhartha Gadgil]

Having just taught and graded a topology course, it is clear that many students should be taught to write proofs clearly (and think clearly as they write proofs). That is indeed the goal here as with Patrick's course.

[Kevin Buzzard]

Kontorivich's ItaLean presentation slides https://github.com/pitmonticone/ItaLean2025/blob/main/presentations/ItaLeanKontorovich.pdf are also worth a look.

[Alex Kontorovich]

Indeed, my course is actually designed not to teach Lean (just as little as absolutely necessary to interact with the system); after the first few lectures, it's almost all Real Analysis... While it's true that I use actual tactics like intro, use, choose, etc (unlike Verbose where those are wrapped in natural language), I actually prefer the precision they offer the students! I now find reading natural language analysis proofs in books to feel similar to reading algebra in the 16th century (as I discuss in the slides which Kevin kindly posted)... My exams are all paper and pen, timed, in-class, and ~80% purely natural language proofs, and 20% actual Lean formal proofs.

[Siddhartha Gadgil]

The question here is whether writing proofs in Lean helps students write better proofs without Lean, and whether having verbose Lean helps with this transition.

[Dan Velleman]

There are some articles that try to address your first question. Here are a couple:
Teaching Mathematics with Lean: Interactive Theorem Provers in the Classroom
Learning about Proof with the Theorem Prover LEAN: the Abundant Numbers Task

[Patrick Massot]

It’s was a fun read. I could see myself six years ago. And then I started developing Verbose Lean to overcome the disappointment.

[Siddhartha Gadgil]

Thanks all. My goal here is not teaching Lean or teaching Analysis, but only teaching writing proofs. Even there we can debate (and should experiment) what works best, but to avoid chaos I will follow verbose Lean, which in my judgement is most promising.

@Patrick Massot I can try to update Verbose Lean as well as the exercises to v4.26.0 next week if you are not working on it now. I find grind is incredibly good with this.

At least with my examples (admittedly for a programming workshop so atypical) I did not need a single rw and in general very few tactics. I had to specify induction, sometimes the correct use of induction, and use if to split into cases. Everything else was grind. @Kevin Buzzard should there be a new version of NNG?

[Siddhartha Gadgil]

As a concrete example, I had to work much harder till not long ago for QuickSort with proofs.

[Kevin Buzzard]

I don't want to go back to NNG myself -- we have plenty of evidence that it works for people, but experience shows that it can be a big time sink and I need to focus on FLT or I'm going to look like an idiot in 4 years' time when I've got nowhere.

[Siddhartha Gadgil]

Kevin Buzzard said:

I don't want to go back to NNG myself -- we have plenty of evidence that it works for people, but experience shows that it can be a big time sink and I need to focus on FLT or I'm going to look like an idiot in 4 years' time when I've got nowhere.

Agreed. I did not mean that you personally battle it again. Just commenting that the style of learning Lean may change where a lot of things we need to do skillfully are automated and the next generation of NNG -like intros may look different.

[Kevin Buzzard]

I would be more than happy for people to experiment with it.

[Siddhartha Gadgil]

With the more powerful grind, Lean is really moving towards where the user provides the high-level guidance and the low level is automated. Should bring in more mathematicians, programmers and better AI.

[Alex Kontorovich]

Yes, that's the viewpoint of the Real Analysis Game; it's currently being refactored to use more powerful tactics as much as possible, while keeping all the "analysis" for the user to do... The only rewrites I want are of the form, e.g.: rewrite [show |1/n - 0| = 1/n by grind], no low-level theorem names...

[Dan Velleman]

I worry that this is too much automation for students who are just learning to write proofs. Such students need to learn how to do some of the low-level steps, so automating those steps may be counterproductive. (For students in Real Analysis, this level of automation may be appropriate.)

[Alex Kontorovich]

It depends how "low level" one wants to go; simply a personal preference that each instructor should decide before proceeding. To teach Real Analysis, I personally do not want to start with the construction of the naturals (or even the reals), I want to go straight to epsilon-delta, and not be bothered with things that are "obvious" to high schoolers but painful to prove from first principles. To each their own!

[Patrick Massot]

I really think grind is not suitable for math teaching. It is simply too powerful. In Verbose Lean, the teacher decides the level of automation. Alex, do you know that in my course students never ever type any lemma name? I tell them: Lean knows the following bunch of facts, and the library takes care of everything I don’t want to see on paper.

[Snir Broshi]

Patrick Massot said:

I tell them: Lean knows the following bunch of facts, and the library takes care of everything I don’t want to see on paper.

So how does it work exactly? aesop? sorry?

[Pim Otte]

Patrick Massot said:

I really think grind is not suitable for math teaching. It is simply too powerful. In Verbose Lean, the teacher decides the level of automation. Alex, do you know that in my course students never ever type any lemma name? I tell them: Lean knows the following bunch of facts, and the library takes care of everything I don’t want to see on paper.

One thing that I've been thinking about is running grind in parallel to tunable automation, in order to give feedback of the form "This fact is true, but you should formulate extra steps" (if grind terminates successfully terminates, but the weaker automation does not", or "This is not true" (if grind proves the negation)

[Alex Kontorovich]

I agree that grind as it currently stands is too strong; I'll need to figure out a way to implement @Patrick Massot's Verbose tactic strengths in my game. That said, we have completely different goals for what we're trying to accomplish (which is perfectly fine! Let's run lots of experiments!). I'm currently refactoring my game and adding some more text. I'm curious to hear what people think about this bit of it:
"
In the 17th century, an algebra problem might read as follows:

You have some unknown quantity. When you create a second copy of this quantity and combine it with a known amount, then multiply this total by your original unknown quantity, you get a specified result.

The mathematics was correct, but the expression was verbose, prone to ambiguity, and difficult to manipulate efficiently. At some point between then and now, we managed to sort out how to replace such paragraphs with the equivalent:

$x(x+a)=b.$

This transition from rhetorical algebra to modern symbolic notation was nothing short of revolutionary. What had once required careful prose could now be expressed in a single, precise line. Variables could be isolated, equations could be solved systematically, and the logical structure became transparent. But note: it takes a nontrivial amount of training (now commonplace, and hence familiar) to understand what exactly those letters arranged in that way mean, and what to do with them in practice.

Today, we find ourselves at a remarkably similar inflection point, but this time in the realm of proof writing. With but a modicum of training in formal mathematics, we can replace verbose, ambiguous, and error-prone prose with precise, compact, and mechanically verifiable formal proofs.

In this text, we not only allow ourselves to write formal proofs, we unapologetically embrace and indeed, celebrate them, not as a pathway for writing good natural language proofs, but as the end goal!

This is a deliberate departure from how formal methods are often introduced. Many excellent projects use proof assistants as training wheels — wrapping tactics in controlled natural language so that students can later transition to writing traditional proofs on paper. That approach makes sense if traditional prose proofs remain the target. But we take a different view: just as no one today laments that students learn $x(x+a)=b$ instead of rhetorical algebra, we are betting that, in the not-too-distant future, people will not lament that students learned to write proofs directly in a formal language. The mathematical community may not quite yet be fully ready for this shift, but the way to get there is to begin.

There is a historical parallel in programming education. For years, conventional wisdom held that students should first learn pseudocode or flowcharts before touching a real programming language — the actual tools were thought too technical, too unforgiving for beginners. Then educators simply started teaching Python directly, and it worked. The intermediate representations turned out not to be load-bearing; they were artifacts of an era when the real tools were worse. Proof assistants have now reached a similar threshold. With modern interfaces, helpful error messages, and the interactive feedback loop of a system like Lean, students can learn to write formal proofs directly — no natural-language scaffolding required.

This text is an experiment. We're wagering that you, dear gamer, can learn to write formal proofs directly, and that doing so will make you a better mathematician, not despite skipping the traditional prose stage, but because of it.
"

[suhr]

I like this idea, but with an additional requirement: a formal proof should be readable without having to interact with a proof assistant. Like, you print it on paper and someone else is still able to read it.

[Alex Kontorovich]

That's what this request was about! :) #Lean for teaching > adding type annotation to `choose` @ 💬

[suhr]

choose is easy to replace though, the lack of type annotations in induction ... with is more painful.

[Snir Broshi]

Alex Kontorovich said:

I'm curious to hear what people think about this bit of it

I love this take, and the Python analogy is cool, but I still doubt the willingness of the math community to adopt such a drastic change in the near future (even 30 years).
Also unfortunately in my experience Lean doesn't have "helpful error messages". I'm not sure this is a requirement for mass adoption as we've seen beginners successfully learn Lean, but most errors I get are very cryptic, similar to C++ compilers exploding every time you forget a semicolon.

[Alex Kontorovich]

Yes, maybe I should go easy on touting helpful error messages... Good catch.

[Alex Kontorovich]

And yes, I say that the math community isn't ready. But this is an experimental step in that direction... (And maybe adoption will happen faster than we think...)

[Jireh Loreaux]

Snir Broshi said:

Also unfortunately in my experience Lean doesn't have "helpful error messages". I'm not sure this is a requirement for mass adoption as we've seen beginners successfully learn Lean, but most errors I get are very cryptic, similar to C++ compilers exploding every time you forget a semicolon.

Whenever you see bad error messages, please shout it from the rooftops. We need to be addressing these, and sometimes it's hard for experts to do because it's hard to remember what you didn't know when you were less experienced.

[Alex Kontorovich]

Do people actually read the error messages in practice? When I get errors, I do things like convert to see where what I've written differs from what I think I'm seeing in the goal state... I rarely find error messages useful...

[Jireh Loreaux]

Yes, always. The errors tell me what I did wrong.

[Jireh Loreaux]

I find using convert in the scenario you describe a nightmare (unless maybe you do using x), because it will try to set lots of things equal for me to prove which are nonsense.

[Alex Kontorovich]

Oh, yes, sorry I use convert iteratively. So first using 1 to see if the big picture worked, and then increase x until I see where the discrepancy is... Maybe somebody should do a little tutorial on how to read error messages effectively? I'd be very happy to learn how others get use out of them