Recordings of Lean coding sessions

Stream: general

[Dylan MacKenzie (ecstatic-morse)]

Are there more videos of people coding in Lean besides Kevin Buzzard's series?

Videos let you see how people approach problems, what tactics they try first, which idioms they use, and generally make you feel better about going slow or getting stuck. I watched quite a few of the Xena Project ones, and found them immensely beneficial. However, it would be good to get a more diverse perspective. Any recommendations?

[Mario Carneiro]

I think there might be some twitch streamers out there, although I forget who...

[Mario Carneiro]

LFTCM (lean for the curious mathematician) is a youtube series arising from an all-online conference with a lot of live coding

[Mario Carneiro]

https://youtube.com/playlist?list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

[Dylan MacKenzie (ecstatic-morse)]

:+1: I watched the infinitude of primes demo but haven't seen the rest. They were above my level at the time, but I expect they will be perfect now.

[Sebastian Ullrich]

Mario Carneiro said:

I think there might be some twitch streamers out there, although I forget who...

geohot :upside_down:
(that was only a single stream, afaik)

[Kevin Buzzard]

So I've put about 25 short videos up in the last month of me just solving basic questions in algebra and analysis, and people watch them. I'd encourage other people to try, there is still not that much information out there about lean and this is a way to see examples

[Kevin Buzzard]

I'll be switching to lean 4 and redoing them the moment we have a maths library. I use linarith and convert and obtain etc all over the place

[Mario Carneiro]

oh, that might be another way to approach the lean 4 tactic prioritization problem: gather a list of the tactics you use most commonly that don't exist

[Mario Carneiro]

(or just a list of the tactics you use period and I can filter out the ones that already exist)

[Mario Carneiro]

since the tactics you use in your videos will be closer to what people actually use on a daily basis rather than what is good for mathlib theory building

[Kevin Buzzard]

Linarith is all over week 2. One problem I face as an educator is what order to do stuff in. I've had great success this term doing basic undergraduate analysis really early -- like Patrick's tutorial. But to do the stuff which our students learn in the first term of analysis linarith is essential

[Mario Carneiro]

Well I can guess the big ones, I'm more curious about the ones you use without thinking

[Kevin Buzzard]

And ring but we have that already

[Mario Carneiro]

you might actually have to check your recordings to see if something is beneath notice

[Kevin Buzzard]

It's the ten basic tactics then linarith and normnum and ring

[Mario Carneiro]

ten basic tactics?

[Mario Carneiro]

do you actually have a curriculum and stick to it in the videos?

[Mario Carneiro]

we already have norm_num and ring, and linarith was outsourced IIRC

[Kevin Buzzard]

Split use cases (and preferably rcases because it makes proofs shorter) left right intro rewrite apply exact have

[Kevin Buzzard]

Rintro obtain rcases would be a bonus

[Mario Carneiro]

rcases is the other big one I think

[Mario Carneiro]

and its variants

[Mario Carneiro]

also cases; lean 4 has cases but it is very different

[Mario Carneiro]

but maybe rcases is a suitable replacement

[Kevin Buzzard]

You can prove natural numbers are a semiring with just induction and rewrite and exact. To prove it's totally ordered you need use intro exact apply rewrite left right and cases

[Mario Carneiro]

Lean 4 also doesn't have the extra bells and whistles of use

[Kevin Buzzard]

Don't need them

[Mario Carneiro]

it has exists (aka lean 3 existsi)

[Kevin Buzzard]

Existsi is fine other than the weird name

[Kevin Buzzard]

And then to start on analysis you immediately need norm_num ring and linarith

[Kevin Buzzard]

And then there are convenience tactics like convert which you can work around

[Kevin Buzzard]

Ext comes up with sets

[Mario Carneiro]

ext is a complicated one

[Mario Carneiro]

apply set.ext is what I did in the old days

[Kevin Buzzard]

https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022/Part_C/Part_C.html

[Mario Carneiro]

nice

[Kevin Buzzard]

Those are the ones I've used so far and I suspect I need very little else

[Kevin Buzzard]

And the logic ones like by_cases are just to make their lives easier

[Mario Carneiro]

Of those in the list, the ones that don't exist yet or only in simplified forms are:

• cases (different)
• ext
• linarith
• nlinarith
• nth_rewrite
• obtain
• rcases
• refl (different)
• rintro
• simpa
• triv
• use

[Patrick Massot]

I would order them as

• use
• linarith
• obtain
• rcases
• rintro
• simpa
• ext
• refl (different)
• cases (different)
• nlinarith
• nth_rewrite
• triv

[Patrick Massot]

Although I don't really know what a different refl means

[Patrick Massot]

I don't think I ever used nth_rewrite or triv

[Mario Carneiro]

different refl means that lean 4 rfl is just exact rfl, not apply all @{refl] lemmas

[Mario Carneiro]

so for example you can't use it to prove x <= x

[Mario Carneiro]

I should also have put "use (different)" since as I mentioned exists exists

[Dylan MacKenzie (ecstatic-morse)]

Kevin Buzzard said:

So I've put about 25 short videos up in the last month of me just solving basic questions in algebra and analysis, and people watch them. I'd encourage other people to try, there is still not that much information out there about lean and this is a way to see examples

I'm one of those people! I've probably seen about 15 in total (I watch them at night if I'm having trouble sleeping). Now I prove things like Kevin Buzzard, except slower and only about basic analysis.

However, I'm wondering if there's some power user techniques that would make life easier. I recently learned about convert and congr, which were very helpful for proving equalities, and I discovered that calc + ring/simp can make things way easier like in #11814. It still feels like I might still be doing things the hard way, though. Is it worth learning conv mode? rewrite_search? Should I be using show more?

[Dylan MacKenzie (ecstatic-morse)]

Presumably the people who maintain Mathlib have figured out which tactics/patterns are useful and which aren't. It would be great to have a condensed "advanced tactics for Mathlib" guide, but putting one together would take time and effort (and might be obseleted in the next year). However, recording your screen while working on Mathlib is basically free (if you ignore the weirdness factor of being recorded), and would allow people like me to extract some useful bits of knowledge.

[Kyle Miller]

I've been recording writing up homework solutions for my number theory course this quarter, and students have been encouraging me to keep doing this since they find value in hearing what I'm thinking when writing them up, seeing how LaTeX works, and observing what happens when I get stuck. Maybe I should make a series for writing up those homework solutions in Lean as well...

[Alex J. Best]

I would say conv is definitely worth learning, and show is important too. I think rewrite search is really cool but don't know if anyone really uses it (I haven't found a situation yet)

[Kevin Buzzard]

Patrick the only reason triv is there is that I decide to introduce true and false very early on in my course, and needed an arbitrary tactic which proved a goal of true -- this is before the students have seen any terms from the library at all like true.intro or whatever. nth_rewrite is there because the canonical question for which it's the answer ("hey, rw changed both my A's to B's instead of just one of them) comes up really early.

[Dylan MacKenzie (ecstatic-morse)]

Alex J. Best said:

I would say conv is definitely worth learning, and show is important too. I think rewrite search is really cool but don't know if anyone really uses it (I haven't found a situation yet)

My first impression was that {squeeze_}simp could do a lot of what rewrite_search does. Not sure if that's correct.

[Dylan MacKenzie (ecstatic-morse)]

I think once you learn conv in (_), there's not much use for nth_rewrite. nth_rewrite is much easier to learn than conv, however.

[Kevin Buzzard]

That's why I teach nth_rewrite. They're having enough trouble in tactic mode at this point...

[Kevin Buzzard]

(deleted)

[Mario Carneiro]

I would say that conv is powerful but fairly niche. You can get by most of the time with just rw with sufficiently specified lemmas, and even if I use conv it is usually in simple ways like conv { to_lhs, rw lem }

[Mario Carneiro]

you have to be facing a pretty hairy goal for conv in (_*_) { ... } to be preferable over the alternatives

[Mario Carneiro]

Should I be using show more?

show is useful for reminding the reader what the goal is which is useful in some kinds of pedagogical tactic style. However it has two other uses, useful even if your only reader is lean:

• show T, from lemma is a way to resolve metavariables in the type of lemma. It is almost interchangeable with (lemma : T), but you might find that show will work in places where type ascription doesn't seem to "stick" because show actually adds an identity function to the term, it's not only used in type inference, and this can sometimes make a difference. This is useful for lemmas that are very generic like dec_trivial, since these could be proving almost anything and you need to specify what you want to prove.
• show T or more commonly change T, when the goal is |- T', can be used to unfold or refold definitions, do beta reduction, or anything else as long as T and T' are definitionally equal. This is very powerful since rather than saying what you want to do as with unfold defn, you say where you want to end up. It can be more verbose than other alternatives if the goal is large, although you can leave lots of underscores in the term. For example if your goal is x + 1 + 1 = (y + 1) - (1/1) + 2 * 2 you can just change x + 2 = y + 4 and lean can prove that this is defeq to the goal.

[Dylan MacKenzie (ecstatic-morse)]

Mario Carneiro said:

you have to be facing a pretty hairy goal for conv in (_*_) { ... } to be preferable over the alternatives

I was using it to rewrite under summations mostly. simp_rw was unfolding some definitions IIRC, although maybe that was simp? I don't remember. Nice to know anyways.

[Dylan MacKenzie (ecstatic-morse)]

I use convert_to pretty frequently, which I think does the same thing but is overkill when things are definitionally equal.

[Kevin Buzzard]

Another use case for show is when your goal is P (x + 2 - 3 + y - x) and you can use rw (show x + 2 - 3 + y - x = y - 1, by ring). This is a nice way to get ring to do exactly the rearrangement you want within a term.

[Joachim Breitner]

Another use case for show is to select one among many open goals, for example if you want to handle them in a different order.

[Joachim Breitner]

oh, rw (show … = …, by …) is neat. Probably better than the

have : … = … := …,
subst this, clear this

(or rw this) idiom that I have been using so far.

[Bolton Bailey]

Kevin Buzzard said:

So I've put about 25 short videos up in the last month of me just solving basic questions in algebra and analysis, and people watch them. I'd encourage other people to try, there is still not that much information out there about lean and this is a way to see examples

Do you have any advice about software for recording/streaming lean proving videos? I've been thinking it might be fun to livestream a "speedrun" of Robbins' proof of Stirling's formula.

[Kyle Miller]

You didn't ask me, but I've had a lot of success with OBS Studio to record parts of my screen along with video of me in the corner (the trickiest part was fiddling with the settings until it no longer got "overloaded," which causes the framerate to drop). When I've needed to edit the video afterwards, I've used Blender of all things -- it was the easiest of all the programs I'd tried on Linux, though you have to look up how you actually export your video since it's not really self-explanatory.

[Kevin Buzzard]

I use OBS Studio too

[Kevin Buzzard]

I never edit my videos, I can't be bothered / don't have enough time.

[Kevin Buzzard]

Sometimes when I'm uploading stuff internally I edit the videos but then I use the infrastructure provided by our VLE (Panopto, in this case)

[Henrik Böving]

I'd do videos / streams of developing doc-gen4 but 90 percent is me grepping through the compiler to find a function that tells me something I want so I don't think that'd be too interesting :sweat_smile:

[Bolton Bailey]

Yes, that seems like a trap you could fall into. My thinking is that, as long as you vocalize your thought process as you look for things, you remain at least somewhat engaging and instructional. I'm pretty good about vocalizing my thoughts even when no one is listening, so hopefully I can apply that and make something engaging.

[Dylan MacKenzie (ecstatic-morse)]

Bolton Bailey said:

Do you have any advice about software for recording/streaming lean proving videos? I've been thinking it might be fun to livestream a "speedrun" of Robbins' proof of Stirling's formula.

This would be great! You'll have at least one viewer :smile:.