Ideas for half-a-year-long undergrad Lean project

Stream: Lean for teaching

[Apurva Nakade]

There is a potential at my university to do a half-a-year-long undergraduate research projects, construed broadly. I'm thinking of proposing some project in Lean. What makes for a good Lean project for undergraduates? It would be great if there is something concrete to show at the end of year. The student(s) will not know anything about Lean or theorem proving at the start but are expected to be good at math.

I know that there is a list of topics missing from undergraduate curriculum in mathlib but I've been burnt before with just picking a topic that "looked easy" and which turned out to be extremely difficult.

I would love to have some advice from people who have done Lean projects with undergraduates. What kind of things/topics work and what do not?

Thanks,

[Apurva Nakade]

@Kevin Buzzard ?

[Scott Morrison]

Unfortunately not joking: things that you've done yourself already. :-)

[Scott Morrison]

(Rather like non-Lean undergraduate projects.)

[Kevin Buzzard]

I've supervised full year lean projects on group cohomology, koszul complexes, perfectoid rings and combinatorial game theory. These were standalone projects written not with mathlib in mind (although Kenny PRed everything mathlib-appropriate to mathlib when doing perfectoid stuff). For me it's a mistake to be too mathlib-focused here. Undergraduates who are good at maths and interested in lean but who have a finite amount of time to do a project don't want (and may well not be interested in) the hassle of the mathlib PR process. I would just take a mathematical topic of the appropriate level and get someone to formalise it. For example one could do higher homotopy groups: that would be a challenge (commutativity of group law for example) but the goal for the student here should be (in my opinion) to prove the theorem, not to get it mathlib-ready.

[Kevin Buzzard]

In fact I have supervised two student projects on group cohomology, each with a more general scope than the last, and then when I finally understood what I thought was the best way to do it I formalised it myself

[Filippo A. E. Nuccio]

And have you already made this into mathlib?

[Kevin Buzzard]

It's on a branch but I never PRed it. It's only the definition of the groups

[Filippo A. E. Nuccio]

You mean that you don't have the connecting homs or you don't have their functoriality (I remember we talked about this but forgot the details... :smile: )

[Kevin Buzzard]

I mentioned it to Scott and he expressed some reservations of the form "why not define it as the derived functor instead" and I got lost trying to prove that it coincided with the derived functir

[Filippo A. E. Nuccio]

But what about Tate cohomology? AFAIK it is not a derived functor on the nose

[Kevin Buzzard]

I don't have anything other than a proof that d^2=0 on some explicit space of cochains. Supervising two projects taught me the least painful way to prove this

[Kevin Buzzard]

Tate cohomology could be done in the same way by adding continuity assumptions everywhere and I agree that it's not a derived functor, unless somehow you can use the pro-etale Scholze stuff to fix this

[Filippo A. E. Nuccio]

AH! I see, you're speaking about Tate's Inventiones Math paper and his vanishing result for cohomology on Tate analytic spaces? I was thinking about $\hat{H}$ for a finite group... :stuck_out_tongue_wink:

[Kevin Buzzard]

Oh sorry, yes those would also be straightforward. They're integer-indexed and I don't understand them conceptually.

[Filippo A. E. Nuccio]

What do you mean by "they would be straightforward"? That they would follow somewhat formally from Scott's suggestion or that it will be straightforward to define them by hand once one has defined (co)-homology via derived functors?

[Kevin Buzzard]

I just meant that defining them as cycles over boundaries would be straightforward. The branch is group-cohomology by the way. The "big theorem" d^2=0, which is here.

[Filippo A. E. Nuccio]

Thanks!

[Kevin Buzzard]

And to try and steer this conversation back on track, that proof came from watching an undergraduate struggle a lot with a more naive proof in an MSc project which taught me a lot but which never went anywhere near mathlib and was never part of a program to fill in a gap in a list of undergraduate mathematics which we don't have yet

[Scott Morrison]

It wasn't meant to be a reservation. :-) "Perfect is the enemy of good."

[Apurva Nakade]

Kevin Buzzard said:

I've supervised full year lean projects on group cohomology, koszul complexes, perfectoid rings and combinatorial game theory. These were standalone projects written not with mathlib in mind (although Kenny PRed everything mathlib-appropriate to mathlib when doing perfectoid stuff). For me it's a mistake to be too mathlib-focused here. Undergraduates who are good at maths and interested in lean but who have a finite amount of time to do a project don't want (and may well not be interested in) the hassle of the mathlib PR process. I would just take a mathematical topic of the appropriate level and get someone to formalise it. For example one could do higher homotopy groups: that would be a challenge (commutativity of group law for example) but the goal for the student here should be (in my opinion) to prove the theorem, not to get it mathlib-ready.

This is useful - not being too mathlib focused. Thanks! This way we could even do different proofs of results that already exist in mathlib.

[Apurva Nakade]

So I'll keep the proposal open-ended in terms of math topics and decide one based on student's backgrounds, and not be too worried about mathlib for now.

[Apurva Nakade]

Another slightly tangential but related questions:

1) Is it possible to do a metaprogramming project if you yourself are not very good at it?
2) Is it worth doing a metaprogramming project now that Lean 4 is imminent?

The Sudoku project is a good example of this. I don't know who did it and what background they had, but I can see something like this being very interesting to students.

[Apurva Nakade]

Scott Morrison said:

Unfortunately not joking: things that you've done yourself already. :-)

Do you mean the math that I've already done or the Lean I've already done? :P

[Kevin Buzzard]

I would actively encourage different proofs of results which already exist in mathlib, because the opportunity is there to write them in a more readable way -- emphasise the pedagogy ("I am a mathematician, I did a project on limits of sequences (or whatever) in Lean, but you can actually learn something about Lean by reading it") rather than the mathlib approach (filter.tendsto.comp or whatever).

[Kevin Buzzard]

I did supervise a metaprogramming project -- Chris Hughes wrote some group theory tactics as his MSc project, however Chris was already a Lean expert and in fact he supervised himself (I guess in fact he asked Mario a lot of questions at some point and Mario taught him -- thanks a lot Mario!) The Sudoku project was done by Markus Himmel, we played with it a bit on the Discord server (if you want to send UG mathematicians towards the Xena discord I'd happily give them invites, some people there know how to use widgets).

[Jake Levinson]

@Kevin Buzzard and @Scott Morrison I read this discussion with interest. I'm considering running an undergraduate research project in Lean this summer; it would be 16 weeks long.

Originally I'd hoped that there could be something small my hypothetical student could contribute to Lean, but my impression is that there are way fewer low-hanging fruit now than there were a couple of years ago. The topics listed above -- higher homotopy groups, group cohomology, etc -- would be a little advanced for my students, who likely do not even know about fundamental groups (though they could maybe learn over the summer). I can probably only assume a handful of proof-based upper-level math classes, perhaps 4-5.

Kevin Buzzard said:

I would actively encourage different proofs of results which already exist in mathlib, because the opportunity is there to write them in a more readable way -- emphasise the pedagogy ("I am a mathematician, I did a project on limits of sequences (or whatever) in Lean, but you can actually learn something about Lean by reading it") rather than the mathlib approach (filter.tendsto.comp or whatever).

This does sound pedagogically valuable, but is there anywhere for a student to contribute their 'more readable' proof? (I'm trying to think of how the student can actually produce something, or have something to show for their work at the end of the summer).

Scott Morrison said:

Unfortunately not joking: things that you've done yourself already. :-)

This makes me wonder, how much background do I need before I can supervise a project of this form? I've never contributed to mathlib and actually find mathlib quite difficult to use (it's so abstract). Most of my experience has come from trying to "roll my own" and redo bits of undergrad math from scratch, e.g. point-set topology (I formalized the basic definitions of fiber bundles).

[Jake Levinson]

Another topic I tried playing with: matroids. But I had to start wrestling with finset vs set.finite vs fintype and that seemed like a tricky design decision to have to make right away. Still, it seemed interesting to me. Do you think this might be a reasonable topic?

One thing about matroids is that there's dozens of equivalent definitions of matroid, so formalizing and proving (some of) the equivalences could be a nice bite-sized contribution and potentially easier than trying to formalize an actual big theorem.

[Jake Levinson]

And one last thing: since Lean seems to tend to be very formal and abstract, are there areas where what's missing is more examples? Say, stuff about dihedral groups, or some standard topological space examples, or "counterexamples in analysis/algebra" type stuff.

[Johan Commelin]

@Jake Levinson Do you know about the matroids project in Lean? https://github.com/e45lee/lean-matroids

[Jake Levinson]

I did not! looking now.

[Heather Macbeth]

Jake Levinson said:

And one last thing: since Lean seems to tend to be very formal and abstract, are there areas where what's missing is more examples? Say, stuff about dihedral groups, or some standard topological space examples, or "counterexamples in analysis/algebra" type stuff.

@Jake Levinson I think this ("examples") is a very good direction, indeed. I had an undergraduate student last summer who indeed did exactly some stuff about dihedral groups (constructing the embedding into the isometry group of the plane), although it didn't make it into mathlib.

[Jake Levinson]

@Heather Macbeth that sounds great! It also seems like a nice way to have new things to do, since it's unlikely that any particular example would have already been 'completely explored' (if such a thing is even possible).

[Heather Macbeth]

A random project which I think would be fun: I made the circle into a Lie group (docs#circle.lie_group), how about making the unit quaternions into a Lie group?

[Heather Macbeth]

Another one: prove the Hermite polynomials form a Hilbert basis for $L^2(\mathbb{R})$ (this could be modelled on my Fourier file)

[Heather Macbeth]

This was another undergraduate project I supervised.

[Jake Levinson]

Heather Macbeth said:

This was another undergraduate project I supervised.

Cool! The pi * r^2 one must have been satisfying to the students.

[Jake Levinson]

How long did that one take to do?

[Jake Levinson]

(I'm assuming the undergrads did not have to prove the FTC?)

[Heather Macbeth]

That was a pretty fast project, perhaps 2 intense weeks over winter break and a month afterwards (occasionally) dealing with reviews to get it into mathlib.

[Jake Levinson]

Wow! I expect know I would be much slower.

[Heather Macbeth]

Jake Levinson said:

(I'm assuming the undergrads did not have to prove the FTC?)

In fact, one of these undergraduates (Ben Davidson) was the author of the easy direction of FTC in mathlib. But he had done this before that project (and it took rather longer).

[Jake Levinson]

Hmm. So this brings me back to the supervisory question -- how skilled I need to be in order to carry out (supervising) such a project. I guess a semi-reasonable answer is "try it and find out".

[Kevin Buzzard]

I was supervising projects from the moment I started learning lean, but of course the better I got at lean the better I got at supervising the projects. At the beginning I'd be supervising students who ended up better than me, but they could always ask their questions here. I run a discord for undergraduate mathematicians; right now I have about 20 students doing projects formalising basic first year undergrad maths and they help each other. The learning curve is steep though.

[Kyle Miller]

Kevin Buzzard said:

and they help each other

This seems to be a valuable aspect of your discord, since having someone who had just recently figured something out can often give a more helpful explanation to someone who is now trying to figure it out than an expert can give. This was something that I found to be useful about the #Berkeley Lean Seminar stream as we started learning Lean.

[Kevin Buzzard]

The big problem with making "get something into mathlib" a target is that the project has to be something which isn't already in mathlib and also has to be written in a certain style which doesn't come easy to all beginners. I have long given up on the mathlib paradigm with generic students and only push people who are strong and have done something which should be in there to go down the hairy path of trying to insert their work

[Kevin Buzzard]

Right now I'm encouraging a bunch of beginners to prove results from their first year analysis course in ways which mathlib would regard as completely suboptimal because they're not using filters (because they don't know what they are). This doesn't bother me in the slightest

[Yury G. Kudryashov]

I'm trying to supervise a student formalizing higher homotopy groups now. It's too early to try to predict outcome at the moment.

[Yury G. Kudryashov]

About examples: there are tons of examples of exotic topological spaces that can serve as counterexamples to converses of theorems

[Yury G. Kudryashov]

It would be nice to have some of them with instances (e.g., encoding negation as is_empty)

[Yury G. Kudryashov]

Then we can have our own pi base

[Jake Levinson]

@Kevin Buzzard I agree, but the question remains, how does the student come away with something to show for their efforts? It is nice for a student's research project to have some kind of deliverable. Maybe it would be enough for them to post their code in a public git repo.

[Kevin Buzzard]

Write some code, write a write-up of what you did either as a pdf or markdown file, dump it in the repo and then get me to add it to the list of student projects on the Xena blog

[Kevin Buzzard]

The student could give a 15 minute presentation about their work and I'd put it on the Xena YouTube channel

[Kevin Buzzard]

That's what Xena is

[Kevin Buzzard]

Unofficial students learning lean for fun and projects

[Kevin Buzzard]

https://youtube.com/playlist?list=PLVZep5wTamMnAF4b66BK0Emxhj5fv-bW_

[Kevin Buzzard]

No deliverable other than a fun summer, a skill learnt, an entry on a CV and a reference from me