Popularisation of lean

Stream: general

[Agamdeep Singh]

Hi,
This is not a technical question and I'm not sure if this is the right place to put it either. Apologies beforehand if it is so.
I'm writing a piece on Lean and how it can take over mathematician's work in the future for an inter-university magazine here in India. Current popular science articles on Lean all seem to have a different approach on what prerequisites to explain.
I'm not as experienced myself to come up with the perfect plan, but the strategy was to elucidate on topics in the following order:
-set theory
-drawbacks in proofwriting/checking process
-type theory
-how it helps Lean as a language

• interactive proofs
• the big proof data base and assisted proofs
  -how essentially in the future Lean could draw from the database of proofs and as an AI deliver theorems/proofs on its own

Please excuse my lack of knowledge and any assumptions I've made that may be wrong.
For an article intended for undergrad and master's students, would you make any changes to the above strategy(article length is about 2000 words)

Thanks a lot.

[Kevin Buzzard]

Some of us believe the dream that one day software such as this will help the modern mathematician in the same way that usual maths packages help them, but I would not be surprised if people have been dreaming this for 30 years and one certainly can't argue that it's happening right now, Lean has given me some insights into undergraduate teaching but has told neither me nor anyone else anything useful about the Langlands Philosophy or anything else fancy

[Kevin Buzzard]

We can dream but it wouldn't surprise me if people have been dreaming for decades. What's different here is that it seems to me that a whole bunch of what I would snobbishly refer to as "proper mathematics" (eg all the advanced BSc and MSc algebra going into lean right now) is all currently appearing in one library in one system, so at the very least the groundwork is being done to make some sort of system which might be able to help people do MSc level algebra in some way. This didn't seem to be happening before, other systems just have a bunch of disparate projects with no underlying goal. But whether this will be a game changer very much remains to be seen

[Agamdeep Singh]

Thanks for taking the time Dr. Buzzard. It was your talk that actually introduced me to Lean.

[Kevin Buzzard]

Right now popularisation is important because it would be interesting to know what happens if eg you type in all the stacks project into lean, and that's not going to happen until we have PhD students doing it for fun

[Kevin Buzzard]

Because the alternative is a multimillion dollar grant focused on doing the job, and maths funders are reluctant to fund such a project because it's not new maths

[Agamdeep Singh]

I completely agree sir. And my generation, which has grown up with computers in their back pockets, does see the fun in that, hopefully we also get to be PhD students.
Is it alright if I quote the message you wrote prior to this one in the article? (just to you know tell people, not get too ahead of themselves either and expect a sentient "Theorem Generator" soon from Lean)

[Agamdeep Singh]

I personally too plan to start contributing to the mathlib database soon.

[Patrick Massot]

I think you shouldn't insist so much about set theory vs type theory. I really don't think this is a key point, it's technical and it's frightening.

[Kevin Buzzard]

When mathematicians use set theory, they use sets to do two distinct jobs -- one solution for two problems. Some of the mathematician's sets are things called Types. For example when a mathematician says "let $R$ be a ring", they mean "let $R$ be a type with a ring structure". But sometimes when a mathematician is talking about a set, they are talking about a subset of a set. For example, theorems about growth of prime numbers might be expressed as "theorems about the set of prime numbers" by mathematicians, but they are actually theorems about the subset of natural numbers which are prime, and its identification as a subset here is crucial -- it gives the prime number a primitive notion of size. But because mathematicians use the word "set" for both these meanings, they find it surprising at first when you tell them that actually every set they ever saw was of this form.

[Kevin Buzzard]

Lean advertises "quotient types" but this is just an implementation detail -- it's easy to make noncomputable quotient types in Lean just by using equivalence classes.

[Eric Wieser]

Is that last remark true? I thought that the design of quotients in lean meant that you could computable compute anything you like with them, and the equivalence class you use only affects the decidability of equality

[Kevin Buzzard]

I don't know, I don't really care about this stuff. All I'm saying is that adding quotients as an axiom the way it's done in Lean doesn't change which theorems you can prove, it just changes which theorems you can prove by rfl.

[Patrick Massot]

Things that you can prove with rfl still make a difference when you have dependent types.

[Kevin Buzzard]

I guess so

[Kevin Buzzard]

but that's only because you're all scared of heq. Chris uses it and says it's fine.