Zulip Chat Archive
Stream: general
Topic: Rich Standard Library?
Speee (Jul 14 2018 at 18:18):
I see that Jeremy Avigad boasts of a rich standard library in Lean here (pdf): https://leanprover.github.io/talks/stanford2017.pdf
For comparison, he notes a bunch of other theorem provers (like Coq and Isabelle) that have, among others, "elementary number theory, real and analysis, point-set topology, measure-theoretic probability, algebra, Galois theory" as part of their standard library.
I assume this is the case for Lean, but I couldn't find anything relevant using the search terms 'topology' and 'lean theorem prover'. I looked through lean/library on github, but it seemed to me very basic.
So is a more sophisticated library non-existent or just hard to find?
Chris Hughes (Jul 14 2018 at 18:41):
https://github.com/leanprover/mathlib
Chris Hughes (Jul 14 2018 at 18:41):
The library's a bit smaller than Coq and Isabelle's libraries at the moment.
Kevin Buzzard (Jul 14 2018 at 19:24):
To give an indication of a few things that are in Lean that might be harder to find in other theorem provers, Lean currently has localisation of commutative rings at multiplicative sets (definitions and universal properties), affine schemes (and also general schemes, although essentially nothing is proved about them), and I'm working on formalising the definition of a perfectoid space at the minute with some others here. On the other hand there are certainly still gaps in Lean's maths library. I think Coq has some basic representation theory and as far as I know we have none of that in Lean. I hope we're not too far from some basic Galois theory but it's not there yet. I am running a summer project with a bunch of undergraduates from Imperial College London where we're formalising random parts of our undergraduate syllabus. It's completely directionless in the sense that the students can just choose to formalise what they like, and many are doing problem sheets from basic courses but some are putting new definitions into Lean. Some students are working on basic homotopy theory for example. I'm hoping we'll do some group cohomology at some point over the summer, and I think we'll get the fundamental group within the next couple of weeks. Is there anything particular you're looking for? Lean is only a couple of years old but it seems to me that the maths library is growing much faster and in more interesting directions than the other provers you mention. I could be wrong though -- I know far less about what is going on in the other provers than what is happening in Lean.
Kenny Lau (Jul 14 2018 at 19:24):
Coq has the whole proof of Feit-Thompson
Kevin Buzzard (Jul 14 2018 at 20:23):
Sure! That's why it has some representation theory; my understanding is that the motivation to develop the representation theory that's there was for Feit-Thompson. But a lot of that huge Feit-Thompson proof can't really be used to do other things, at least that's my understanding of it -- it's just lots of technical lemmas about group actions and maximal subgroups etc which are used only to prove F-T. Of course one might use F-T to prove other things.
Kevin Buzzard (Jul 14 2018 at 20:24):
Lean might have a statement of the local Langlands conjectures for tori. @Kenny Lau -- does it have a sorry-free statement nowadays?
Kenny Lau (Jul 14 2018 at 20:29):
not really
Kevin Buzzard (Jul 14 2018 at 20:38):
What needs doing? How hard is the absolute Galois group? We have existence of maximal ideal of a non-zero ring -- is constructing alg closure still a lot harder?
Kenny Lau (Jul 14 2018 at 20:39):
I just feel like there's a huge barrier although I can't tell you what it is
Kenny Lau (Jul 14 2018 at 20:40):
should we develop enough machinery so that we can prove that K1 is already algebraically closed?
Kenny Lau (Jul 14 2018 at 20:41):
structure theorem for inseparable polynomials: every polynomial f(x) is of the form h(x^(p^n)) where h(x) is a separable polynomial and p is the characteristic of the field, under the convention char Q = 1
Kenny Lau (Jul 14 2018 at 20:42):
8 definitions of a perfect field
Kevin Buzzard (Jul 14 2018 at 20:42):
What's the point?
Kevin Buzzard (Jul 14 2018 at 20:43):
At the end of the day I am interested in a definition of the algebraic closure, not a tricky theorem about how it can be written in a different way
Kenny Lau (Jul 14 2018 at 20:43):
you wouldn't teach someone LCFT if that someone doesn't know what a separable polynomial is, that's the point
Kevin Buzzard (Jul 14 2018 at 20:43):
I am not so sure about that
Kevin Buzzard (Jul 14 2018 at 20:43):
there are plenty of people who only care about applications to number fields so assume char 0 everywhere
Kenny Lau (Jul 14 2018 at 20:44):
"separable polynomial" was an example for more basic knowledge
Kevin Buzzard (Jul 14 2018 at 20:44):
Oh I see.
Patrick Massot (Jul 14 2018 at 20:47):
Are you still working on the perfectoid project?
Kevin Buzzard (Jul 14 2018 at 20:48):
I've not even thought about it for the past two weeks -- I've been very busy with undergraduate level maths. I'd really like to get back to it.
Kevin Buzzard (Jul 14 2018 at 20:49):
Today I had two hours to kill so I spent some time on my book. I just have more Lean projects to do than there are hours in the day at the minute.
Kenny Lau (Jul 14 2018 at 20:49):
Patrick Massot (Jul 14 2018 at 20:49):
I understand you've been busy. I'm only asking if you still want to pursue this or prioritize other projects
Kenny Lau (Jul 14 2018 at 20:49):
and as for me, I'm now half way through
Kenny Lau (Jul 14 2018 at 20:49):
(never mind, I can't maths)
Kenny Lau (Jul 14 2018 at 20:50):
I'm almost half way through
Patrick Massot (Jul 14 2018 at 20:50):
half way through what?
Kevin Buzzard (Jul 14 2018 at 20:50):
My last hold-up was that I needed to prove several definitions of valuation were equivalent, and then discovered that we didn't even have quotient rings and that R/P was an integral domain if P was prime.
Kenny Lau (Jul 14 2018 at 20:50):
Atiyah-Macdonald
Kevin Buzzard (Jul 14 2018 at 20:50):
I definitely want to pursue it and I saw your work on completions
Patrick Massot (Jul 14 2018 at 20:50):
Reading or formalizing Atiyah-Mcdonald?
Kenny Lau (Jul 14 2018 at 20:50):
reading
Kenny Lau (Jul 14 2018 at 20:51):
unfortunately
Patrick Massot (Jul 14 2018 at 20:52):
Ok. Hopefully I'll work more on completions. It should be doable and not too long
Kenny Lau (Jul 15 2018 at 17:26):
the point is that we have two definitions of a separable extension:
1. the usual one
2. the one involving tensor products
and one of them is more useful than the other, but one of them is quicker to define
Kenny Lau (Jul 15 2018 at 17:26):
the point is that you don't want to just define a bunch of stuff and rush the goal
Speee (Jul 17 2018 at 21:49):
Thanks! So given the relative poverty of the library, what are some reasons to choose lean for my formalizing needs anyway?
Kevin Buzzard (Jul 17 2018 at 21:50):
That would depend very much on your formalizing needs I guess. I use it because it's fast, it has a cool community here, and the unicode looks good so mathematicians find it less scary
Mario Carneiro (Jul 17 2018 at 21:56):
In what sense relative poverty? Are you coming from a particular theorem proving community?
Kevin Buzzard (Jul 17 2018 at 21:56):
Yeah, we're the only guys with schemes :P
Mario Carneiro (Jul 17 2018 at 21:57):
I'm concerned that Speee is referring to the core lib which is quite impoverished but is far from all there is in lean
Speee (Jul 17 2018 at 22:10):
I do prefer readability most of all (and Lean shines here), but I could use a mature library to compare my own attempts against. It's nice to see an active community though, as that can provide the kind of feedback I'm looking for!
Mario Carneiro (Jul 17 2018 at 22:11):
I don't know how mathlib rates on maturity, but there is certainly more than enough for comparing your own work against
Last updated: Dec 20 2023 at 11:08 UTC