Help me sell Lean to my professor

Stream: general

[Rida Hamadani]

Tomorrow I will be meeting with my combinatorics professor, for the purpose of telling him about lean.

I would really appreciate it if you could give me ideas to present to him tomorrow in order to convince him of the importance of formalization in general, and with lean in particular.

I'm aware this has been discussed before, I read some arguments on the Xena project blog for example, but my hope here is to find arguments that would convince a combinatorialist specifically, although more general advice is appreciated too.

[Arthur Paulino]

I think it really depends on the goal of your presentation, that is, what you'd expect as an "adoption success".
Some professors in this community have been using Lean to teach undergrads, giving them assignments etc. I'm sure Patrick and others can tell you plenty about that.
There are also formalization projects led by some professors (and maybe some projects led by students?). Heck, if I were studying mathematics, I would love to be involved in some project like this. Not necessarily to develop cutting edge mathematics... just to be less of a loner and to improve my coordination skills.

There are of course adoption barriers. Some professors may not want to change their ways of teaching, maybe for good reasons (they might have perfected it through decades) or maybe for bad reasons (they might just dislike changing even when things are going sideways). Also, some students may dislike the experience of doing the setup, sometimes talking to a computer terminal, or simply learning the tactics DSL

[Kevin Buzzard]

@Bhavik Mehta is giving a talk about combinatorics in lean tomorrow in Singapore (in just over 12 hours' time); ask them for their talk slides and borrow from them! Also check out his Xena Project blog post about formalising combinatorics, it's one of the most recent posts there. Also check out Tao's AMS talk from January on YouTube, the one on formalisation. Or get your combinatorics professor to watch it! Sorry no links, on mobile right now :-(

[Rida Hamadani]

Thank you very much, I'll check out these resources!

[Rida Hamadani]

Arthur Paulino said:

I think it really depends on the goal of your presentation, that is, what you'd expect as an "adoption success".

Any progress towards making "formalizing mathematics" a thing in my university would be a good step. In a perfect world, I would be able to convince my professor to formalize some paper he finds particularly important, maybe as the thesis of some masters student, or perhaps have a talk about lean in the next conference that occurs at the university.

[Jireh Loreaux]

Patrick Massot's why formalize mathematics is excellent.

[Rida Hamadani]

Thank you, I will check it too.

[Bhavik Mehta]

One link from me: https://www.youtube.com/watch?v=WimtCW8Qn2U was to the additive combinatorics webinar, on an older project. Some specific examples aren't covered by anything so far but I think are interesting:
1) The snark conjecture is a big conjecture (which implies the four colour theorem) but its proof has been announced by well-known researchers in the area, but the proof is mostly unpublished and its status is therefore wildly unclear. Formalisation of something like this would be difficult but if organised possibly together with the authors, would be cool. Provided the authors are interested and there's enough community momentum (come formalise a different proof of the four colour theorem that's stronger!), I'd argue this is also feasible given the rate combinatorics can be formalised (cf ramsey project, PFR) and the success in formalising a "moving target" with authors' help (cf ConNF)
2) Formalisation of a theorem can help understanding / fixing it, both for students and for the authors! In unit-fractions, some of the constants inside theorem statements were changed for formalisation (in a way which doesn't affect the main result, but were technically incorrect as written) but would be subtle to notice unless you were looking very closely. I understand Scholze commented during LTE that seeing the formalisation procedure helped him view the proof in a conceptually different way (don't quote me on this one, but I'm sure someone else can find the quote). For Ramsey, I wanted to formalise it mostly because I thought it was a cool proof that I wanted to understand (which I now do).

[Rida Hamadani]

Awesome! Thank you for mentioning the snark conjecture, this sounds like a great project to work on even if I didn't find success in convincing my professor.

[Bhavik Mehta]

Also: https://youtu.be/ywJF4as9ocA?t=3250

[Jeremy Avigad]

This special issue of the Bulletin of the AMS may help:
https://www.ams.org/journals/bull/2024-61-02/?active=current

[Shreyas Srinivas]

All the above resources are a good idea, but the key to the selling part is to make the fruits of formalisation relatable to your prof and show them that formalisation addresses something they care about or a meta-problem they face at their work. If you emphasise the "checking the correctness" part heavily, then you risk giving them the impression that formalisation is essentially concerned with working out minor details of proofs and checking them.

[Patrick Massot]

Shreyas this is one reason my text that have been cited is not emphasizing this “checking correctness” aspect.