scope of mathlib

Stream: general

[Arthur Paulino]

Johan Commelin said:

I don't think that should be out of scope. Sure, we can't do that now. But we shouldn't paint ourselves in a corner. It's good to look far ahead (-;

Sorry for sidetracking, but is there something in the mathematical academic world that's out of the scope of mathlib? or is it the case that mathlib could eventually reach state of the art math research on (almost) every field?

[Notification Bot]

This topic was moved here from #maths > Distribution theory by Johan Commelin

[Johan Commelin]

@Arthur Paulino My personal opinion is that 99% should be in scope in theory. Of course it's a cool challenge to do this in practice. For that we would need to scale up massively. And that's what we are trying to do.

But some stuff might be out of scope.

• There's a bunch of maths that is completely out of fashion. I don't think we should spend a lot of energy on trying to support that.
• Some maths is so imprecise that it's unclear if it can ever be formalized in its current form. For example, Hales commented in his Big proofs talk that he didn't know how to formalize the Milleniums problem statement for Yang Mills. I guess, what I'm saying is that some conjectures are so imprecise, they are out of scope for formalization.
• I don't think we'll have native support for alternative logics or foundations anytime soon.

[Arthur Paulino]

I see. So anything that's interesting and precise enough could very well part of mathlib someday

[Kevin Buzzard]

Anything which is precise enough could be done in Lean, however mathlib has made its intentions clear -- we are focussing on the kind of mathematics which is happening in maths departments in 2022 (both in the undergraduate lecture theatre and in the researcher's office) for the simple reason that this is the stuff which is important to mathematicians in 2022.

[Kevin Buzzard]

There are plenty of dusty old books in our library which nobody has borrowed for 50 years

[Kalle Kytölä]

Kevin Buzzard said:

...happening in maths departments in 2022 (both in the undergraduate lecture theatre and in the researcher's office)...

Undergraduate lecture theatres? That's so 2019. In 2022, undergraduate lectures are happening from the researcher's office. (Ok, ok... Let's hope we'll soon be back in the theatres!)

[Martin Dvořák]

Do we draw a line between Math and Computer Science? I prefer not to; however, my opinion is not the one that matters.