Zulip Chat Archive

Stream: general

Topic: stacks project / schemes


view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:13):

Thought this was worth its own topic because we all know there are people here who are less interested in the maths side of things. Here's an update.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:14):

Kenny and I nearly have schemes. Not in a "just about ready for mathlib" sort of way -- far from it -- but in a "the mathematically correct definition" sort of way.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:16):

It will need a lot more work before it goes anywhere near mathlib, but I am not going to do that work quite yet because for deadline reasons it would be nice to get perfectoid spaces before 10th March, or at least to get some way towards them. After that we can think about tidying up and deciding which bits mathlib might want and in what form.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:18):

The reason I'm posting is because I need to make a call on categories. At the end of the day I currently need sheaves of commutative rings (for the _definition_ of a scheme), and to actually prove anything at all I need sheaves of modules for these rings. For perfectoid spaces I will need sheaves of topological rings on a site.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:18):

So do I go with sheaves taking values in categories or do I just muddle on?

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:19):

If I go with sheaves taking values in categories then to put it bluntly it simply raises the bar even higher to getting anything in to mathlib.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:19):

Now Patrick has urged to me to get this into mathlib-ready form, and I'll start on this after the 11th.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:19):

Here's a question: what is the least common denominator of all the things you need sheaves of?

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:20):

My hope is that it is at least a concrete category

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:21):

If you project needing 3+ different kinds of sheaves, that's sufficient for making a single generalization, but it's not immediate that this generalization should be over categories in the usual sense

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:22):

But this has always been an independent experiment for me -- can we actually even define a scheme / perfectoid space in Lean? For me that is an interesting independent question. I don't think it is for Mario, because he looks at maths very differently and, not unreasonably, I don't think he can tell the difference between a perfectoid space and a topological space in some sense -- they're both structures with a bunch of axioms to him. And for some reason he seems very much focussed on theorems rather than definitions -- a theorem for him is proof that the definition works, whereas if I know as a mathematician that a definition is correct then for me that might be enough.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:23):

So there is certainly the possibility that my conclusion is "look, here's a definition" and Mario's response is "who cares?". And the definition might just then sit there for months just being something that mathematicians can look and go "oh look what they can do now, how fancy, that's a million miles from the odd order theorem isn't it".

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:24):

The Least Common Denominator depends very much on how far you want to go.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:24):

I think you are right in that assessment. It seems to me obvious that one can make a definition of scheme / perfectoid space in lean; that's obviously within Lean's capabilities. The question is only if one can make a good or useful definition

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:24):

The Weil Conjectures are a famous theorem.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:25):

For them you ideally would have sheaves on a more general object than a topological space and then take the derived category.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:25):

My gut feeling is that by that point you want to be using categories.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:25):

by that point...

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:25):

I don't think you should be afraid of later revision

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:26):

have goals, and plan for them. If you want the Weil Conjectures, then go for it

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:27):

I think you are right in that assessment. It seems to me obvious that one can make a definition of scheme / perfectoid space in lean; that's obviously within Lean's capabilities. The question is only if one can make a good or useful definition

No, that's just one question. Another question is how to get mathematicians talking about Lean. And we already have ample evidence that proving a theorem which is 400 pages of ingenious but relatively straightforward calculations in group theory and which was done by mathematicians before all of us were born, does not do it. But in the math community there is huge excitement about perfectoid spaces because they are new and they are demolishing bits of the Langlands Programme which people thought were hitherto inaccessible. They are fashionable.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:27):

Is there positive evidence that writing down a definition will interest mathematicians?

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:27):

This is the part that you (Mario) cannot see at all and this is unsurprising given where you are sitting and your background

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:28):

There is positive evidence that not writing down a definition will not interest them.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:28):

In a sense it seems much the same as proving an old theorem formally - whoop-de-doo you formalized a definition we all know

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:28):

I am going to give a talk at an undergraduate conference on the 11th, a theoretical talk, an introduction to perfectoid spaces and what they can do

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:29):

and I think it would be cool to unveil the definition there.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:29):

There is a difference which you can't see.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:29):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:30):

Making a _new_ definition which is extremely complex and most mathematicians don't understand has much more of an air of mystery about it.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:30):

There is a subtlety.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:31):

I assume that perfectoid spaces are not themselves the object of perfectoid theory, such as it is. Presumably they are being used in some way to get things done, some proof strategy that harnesses the power of the definition

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:31):

Currently the word "perfectoid space" to most mathematicians means "abstract structure whose definition I have not read and would probably not understand if I did read, but I know that in the number theory community everyone is talking about them and I get the feeling that there is a general sense of excitement happening right now"

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:31):

this is absolutely absolutely the opposite of everyone's feeling about the odd order theorem

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:32):

I'm obviously in the wrong place to make such pronouncements, but I won't be convinced you've done a thing with substance until you mimic such proofs

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:32):

Well there is a basic "perfectoid theory" which was only worked out a few years ago

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:32):

Mario I am not suggesting I have done anything of substance with perfectoid spaces even if I manage to define them.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:33):

But I am suggesting that they might be a selling point.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:33):

Because in contrast to the odd order theorem, which everyone understands and nobody cares about

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:33):

I freely admit I don't understand what makes a thing a selling point for mathematicians

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:33):

perfectoid spaces have the property that nobody understands them and a lot of people care about them.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:33):

I freely admit I don't understand what makes a thing a selling point for mathematicians

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:34):

Right, it's all just structures to you.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:34):

It would be like me saying "OK so you wrote a search engine and you wrote a space invaders game, they're all just computer programs at the end of the day though"

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:34):

if I just couldn't tell the difference between them

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:34):

because I never used either of them

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:35):

I don't expect you to see any difference between the definition of a group and the definition of a perfectoid space

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:35):

however I do think you should know that one is more fashionable than the other currently, in some circles.

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:36):

Currently the word "perfectoid space" to most mathematicians means "abstract structure whose definition I have not read and would probably not understand if I did read, but I know that in the number theory community everyone is talking about them and I get the feeling that there is a general sense of excitement happening right now"

I can confirm this.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:36):

Okay, by that analogy the proofs is where you "run the program" of the definition, that's where the differences become obvious

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:37):

Otherwise I'm just staring at a bunch of code for space invaders / google, and I don't understand what does what or why

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:38):

Right

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:39):

But on the other hand if you are in a community and there's a whole bunch of other people that you respect getting very excited by some computer program which you are not competent enough to use, then this might rub off.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:40):

And if you're then on some grant committee that is deciding where the money is going and you see a proposal which mentions this fancy new program which you know there are experts raving about then perhaps you are favourably inclined towards that proposal even though you can't actually understand it.

view this post on Zulip Mario Carneiro (Feb 28 2018 at 09:40):

I think you need to get famous number theorist X involved in your project then

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:40):

I think I should write the definition first!

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:41):

I think you need to get famous number theorist X involved in your project then

Yeah, who has Scholze's phone number?

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:41):

That would have an impact

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:41):

I exchange emails with him from time to time

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:41):

but I've not mentioned this to him yet.

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:41):

Imagine Peter Scholze in Rio explaining he is now using Lean as a day to day tool

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:42):

That is not going to happen, but when I finish it I will certainly mention it to him.

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:42):

[Note to non-mathematician: Rio is where Scholze will get his Fields medal this summer]

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:42):

It would be interesting to hear his opinions.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:43):

The non-mathematicians have all muted this thread ;-)

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:43):

Damn Zulip!

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:44):

This is exactly the sort of chat that takes up 200 messages on gitter and all the poor CS guys just have to scroll through and hope that they see the CS question somewhere in the middle that we all ignore

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:44):

I think that if we figure out how to make these topics work properly then it might be of benefit to everyone.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:45):

Anyway, Patrick and Mario I suspect you have different opinions on this issue. Let's imagine I triumphantly define a perfectoid space structure at 4am on the morning of 11th March and then decide to move on to something else for a month

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:46):

and it's manifestly not mathlib-ready and I don't have the time to even prove Lemma 1 about perfectoid spaces

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:46):

Mario is then manifestly not interested in adding the definition to mathlib, and he has explained his reasons above.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:46):

Patrick would you be happy with it just sitting there in some random repo on my github?

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:47):

a valid but potentially unusable definition?

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:47):

I wouldn't be happy, but who cares?

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:47):

My plan is to make the definition and then just tell a bunch of undergraduates about it

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:47):

and maybe some graduate students

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:47):

until I find one or two people who are interested in taking it further.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:48):

Undergraduates do do pretty weird things nowadays.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:48):

Probably people have seen MO questions of the form "I am an undergraduate but I have been reading Lurie's book and I have a question about infinity-categories"

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:49):

and sometimes the questions are just plain stupid

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:49):

but sometimes they are graduate student level

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:49):

For me this is evidence of a big change in the way people are accessing and learning mathematics.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:49):

Undergraduates have access to so much information now because of the web, so they find random things and attempt to engage with them.

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:49):

But this will happen one month after your talk. And by that time your lone repo won't be compiling against current Lean

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:50):

I don't care

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:50):

because I am going to fix this problem if necessary by fixing which version of Lean I am using

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:50):

I would really really love for Leo to release 3.4.0. I would stick there like a shot.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:51):

I am going to make a bunch of teaching material which will all run on some fixed version of Lean and then actively urge the undergrads not to upgrade.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:51):

That's why I am excited about the project which is going to make old nightlies accessible.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:52):

I just think that for certain people, a formal definition of a perfectoid space will be a really interesting looking carrot.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:53):

Schemes was enough of a carrot for Kenny, for example.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:54):

But actually I came here to ask whether I should use @Scott Morrison 's category theory library or whether it's not yet ready. That's the call I have to make at the minute.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:54):

If all I want is schemes then all I need is sheaves of rings which I can do by hand.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 09:54):

But this doesn't scale.

view this post on Zulip Patrick Massot (Feb 28 2018 at 09:55):

People who care about schemes or perfectoid spaces will want the latest advances in Lean automatisation. They won't be happy with Lean 3.4.0

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 10:04):

I see.

view this post on Zulip Patrick Massot (Feb 28 2018 at 10:42):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

Come on @Assia Mahboubi fight back!

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:23):

@Kevin Buzzard, agreeing a bit with @Patrick Massot , I do think it's important that developments end up in mathlib (or otherwise in repositories with multiple contributors who may maintain things). In the current Lean ecosystem, bitrot happens incredibly quickly (in fact so much so that I think I actually agree with Leo --- possibly all of the current mathlib is doomed to need complete rewriting several times over in the next few years).

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:27):

It leaves me genuinely uncertain about the best path. I think you're fundamentally right in wanting to make a dash towards an important and impressive part of modern mathematics. I agree with everything you say concerning the odd order theorem. (The initial human proof of the odd order theorem was in some ways a huge disappointment --- it was one of the first times humans encountered an interesting theorem whose shortest proof was really long. Saying that computers are helpful for doing tedious mathematics is not really a selling point.)

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:28):

But I'm also pretty sceptical that the March 11 dash you have in mind is going to have much effect. It's too likely that the code will fall apart quickly afterwards, or otherwise be unusable because it was written hurriedly.

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:32):

I would like it to have an effect --- what we should dream about is a "mathoverflow effect", whereby one day a new thing appeared in the world that everyone realised they'd always wanted. I think there are potentially a huge number of students out there who would be interested in contributing to Lean libraries. However in combination with any "publicity", we would also need to have better strategy in place for teaching them how to work in Lean, and to productively organise their work. The current Lean community is realistically not yet ready for either of those.

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:33):

It's great that documentation is coming along. TPIL is a great resource, and it's fantastic to see the mathlib documentation growing.

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:34):

Unfortunately writing good Lean code is really hard (I still write lots of crappy code, after 18 months of learning Lean), and so any influx of new people could potentially just overwhelm those people in the community who can actually review PRs.

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:35):

Finally, to try to answer your question, @Kevin Buzzard, I am trying to get the category theory library ready to PR into mathlib. But collaborators and postdocs and students are starting (ha!) to notice that I'm not getting much maths done...

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:38):

Hearing you wanting it of course motivates me, for better or worse. I think building good foundations (e.g. using category theory to avoid proving everything 5 times over when setting up algebraic geometry) will be really helpful.

Also, I'm still a little proud of how few proofs I have in my library (i.e. how many are proved by obviously with little or no human intervention). :-)

view this post on Zulip Scott Morrison (Feb 28 2018 at 11:39):

Oh -- and in some interesting news -- two mathematicians here at ANU, after coming to my undergraduate students' talks (on implementing Euclidean domains, and the first iso theorem for groups), said they were going home to install Lean over the weekend. There's hope. :-)

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 11:56):

I would like it to have an effect --- what we should dream about is a "mathoverflow effect", whereby one day a new thing appeared in the world that everyone realised they'd always wanted. I think there are potentially a huge number of students out there who would be interested in contributing to Lean libraries. However in combination with any "publicity", we would also need to have better strategy in place for teaching them how to work in Lean, and to productively organise their work. The current Lean community is realistically not yet ready for either of those.

I am going to dedicate a lot of time over the summer to writing documentation for undergraduate mathematicians introducing them to how to use Lean via my introduction to proof course.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 11:58):

Proving an _old_ theorem formally -- you formalised a theorem that we all understand the statement of and which was proved before we were all born

Come on @Assia Mahboubi fight back!

Ha ha! I was of course taking a very extreme viewpoint which I do not 100% believe in myself. I just wanted to highlight some of the obvious differences between defining a perfectoid space and proving the odd order theorem, even though "they're both computer programs".

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:34):

Hi @Patrick Massot ! Thanks for having pointed me to this new forum and thread!

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:37):

Hi @Kevin Buzzard ! Thanks for this thread, it's extremely interesting. And no worries about the assessment of the odd order theorem: in fact,
I agree with many of the points you make.

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:39):

Fortunately, I was told what a perfectoid space is 2 weeks ago, otherwise I wouldn't have dared joining the discussion :-).

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:48):

I agree that the fact that it was possible to write down a formal proof of the odd order theorem only demonstrates that proof assistants can be used to represent good old undergraduate level algebra. Not that proof assistants are useful tools for research in mathematics.

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:51):

Even if in fact parts of the proofs involve slightly more advanced representation/character theory, etc.

view this post on Zulip Patrick Massot (Feb 28 2018 at 13:56):

Fortunately, I was told what a perfectoid space is 2 weeks ago, otherwise I wouldn't have dared joining the discussion :-).

Hi Assia! That's the point: Kevin wants to formalize stuff that mathematicians think are cool and intimidating

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 13:58):

My hope is that one day proof assistants will be useful to discover new stuff, because the computer can in principle help you play with the definitions, discover abstractions and test them. So yes, I agree, it would be really cool to have the definition of a perfectoid formalized, because then one could play with it interactively instead of staring at a paper definition like a fish out of water.

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 14:01):

But then I am not sure that the main problem is to come up with a definition which is not usable. I would say that the problem would be to formalize what a cat is and then to call it a perfectoid. Specially if not many people both know what a perfectoid is and how to speak/read Lean.
Lean checks proofs but only human readers check the definitions. So a collection of theorems, and of convincing examples, helps this assessment.

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 14:11):

As a regular reviewer of papers about formalized mathematics, I often read papers which claim to formalize the theory of mystuffoids, it is very interesting and the authors prove a litany of lemmas, culminating with the Fundamental Theorem of Mystuffoids. But the authors never provide a (formalized) instance of mystuffoid. So as a reviewer, I try to verify that all the elementary examples of mystuffoids I know of can indeed by equipped with the structure provided by the authors. And that a few things that are not stuffoids for a good reason will not be instances. I had myself issues with my own tentative formal definitions at several occasions, and rejected several papers because this protocole made explicit flaws in the definitions.

view this post on Zulip Patrick Massot (Feb 28 2018 at 14:28):

I'm afraid there is no "elementary example" of a perfectoid space :wink: And my daughter woke up, I need to rush to ski

view this post on Zulip Assia Mahboubi (Feb 28 2018 at 14:33):

Enjoy!

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 20:37):

But I'm also pretty sceptical that the March 11 dash you have in mind is going to have much effect. It's too likely that the code will fall apart quickly afterwards, or otherwise be unusable because it was written hurriedly.

Listen. I am in this unique position in that I get to give a lot of talks about a lot of random things to lots of people most of whom are under the age of 20 and some of whom are extremely smart. I am personally, after many conversations (and I'm sure Patrick feels the same way) no longer really interested in telling research mathematicians about formal theorem provers, because generally they are not interested. But on the other hand undergraduates are interested, and if you train them right they can really do stuff. Chris Hughes is answering other people's questions on this chat now and we all know what Kenny has done. There are other people "bubbling under" in my Thursday evening meetings and I'll train them up too. Remember that when those undergraduates started coming to my club I could not even use the software. I could not prove 2+2=4 in the reals, and nobody could prove anything about the complexes because there were no complexes. And yet a few people stuck around and are doing interesting things. Next year I am going to be a lot better and let's see what happens. But back to this conference. I think that if you're a smart 20 year old and you come to my talk on the 11th at some undergrad pure maths conference to learn about perfectoid spaces and then you hear me say that I've defined them in Lean and if you want to learn about Lean then you might want to try proving lemma 1 about them, then there is a chance that you will get curious and try. I do think there's a chance. And if you fail, which of course you might well, then you might instead want to try some of the easier lessons on my blog. And then you might get addicted, like I did and like Chris did. So I am going to continue going round the South East of the UK telling undergrads and schoolkids about Lean because there are random smart people out there who are bored at uni and who might actually want to goof around with trendy objects in a theorem prover. Maybe. I am genuinely trying to piggy back on the trendiness of the topic. I've written a paper about perfectoid spaces so I do have an excuse to talk about them, why shouldn't I tag Lean on and see what happens? I want to push undergraduates -- who don't know any better -- to start investigating theorem provers, because I think they're the future of pure mathematics and I think that thus far the CS community has singularly failed to demonstrate this to the maths community. I am trying a new idea from a new perspective, purely for fun. I want to introduce them from the bottom up and I am prepared to try lots of angles, and for me perfectoid spaces is definitely an angle worth trying. I want to try 10 different things and this is one.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 20:43):

As a regular reviewer of papers about formalized mathematics, I often read papers which claim to formalize the theory of mystuffoids, it is very interesting and the authors prove a litany of lemmas, culminating with the Fundamental Theorem of Mystuffoids. But the authors never provide a (formalized) instance of mystuffoid. So as a reviewer, I try to verify that all the elementary examples of mystuffoids I know of can indeed by equipped with the structure provided by the authors. And that a few things that are not stuffoids for a good reason will not be instances. I had myself issues with my own tentative formal definitions at several occasions, and rejected several papers because this protocole made explicit flaws in the definitions.

Oh this is a _great_ comment! Because basically it is pointing out that until I prove some lemmas, people can just say "how do you know you have the right definition?". I am not sure that undergraduates have the guts to say that ;-) but still this comment sticks in my head. So in fact I have to prove some lemmas just to check.

view this post on Zulip Kevin Buzzard (Feb 28 2018 at 20:45):

I'm afraid there is no "elementary example" of a perfectoid space :wink: And my daughter woke up, I need to rush to ski

I think the empty space is perfectoid. I'm not sure that it highlights the key features though.

view this post on Zulip Sean Leather (Mar 01 2018 at 06:28):

Oh this is a _great_ comment! Because basically it is pointing out that until I prove some lemmas, people can just say "how do you know you have the right definition?". I am not sure that undergraduates have the guts to say that ;-) but still this comment sticks in my head. So in fact I have to prove some lemmas just to check.

@Kevin Buzzard: I interpreted the comment not as saying “prove some lemmas,” but as saying “give examples.” In other words, don't just give a definition and lemmas, but show that there are things that instantiate your definition. Otherwise, your lemmas might be wonderful but never be of any actual use.

view this post on Zulip Kevin Buzzard (Mar 01 2018 at 07:28):

In fact for the definition I'm going to give, it will be really hard to give any examples, because we're going to cut corners and possibly come back later.

view this post on Zulip Patrick Massot (Mar 01 2018 at 08:46):

@Kevin Buzzard: I interpreted the comment not as saying “prove some lemmas,” but as saying “give examples.” In other words, don't just give a definition and lemmas, but show that there are things that instantiate your definition. Otherwise, your lemmas might be wonderful but never be of any actual use.

@Sean Leather I hope you realize you are being really rude here. We are talking about Algebraic Geometry and Langlands Program here, giving an example would be a disgrace. If needed, google "Grothendieck prime number 57".

view this post on Zulip Sean Leather (Mar 01 2018 at 08:56):

I hope you realize you are being really rude here. We are talking about Algebraic Geometry and Langlands Program here, giving an example would be a disgrace. If needed, google "Grothendieck prime number 57".

@Patrick Massot: You're right. I'm so accustomed to using the programs I write that I forget about mathematicians not needing to use the theorems they prove. :sweat_smile: I'm completely out of my depth here, and I apologize for any unintended insolence. :innocent:

view this post on Zulip Kevin Buzzard (Mar 01 2018 at 09:37):

@Sean Leather I thought about your comment a bit more and it's more complicated than I first imagined. Somehow examples and lemmas all get mixed together in this game, and definitions too. It's a bit strange. I said to Mario earlier "for you there is no difference between a perfectoid space and a group, they're both just structures" but somehow this isn't right. A group really is just a structure defined by some axioms. For these more complex objects there are theorems that you need to prove before things even make sense. For example you sometimes want to say "and my structure has an X, and if we choose a generator f of X then f also has property Y" or maybe even "and for all generators f of X, f also has property Y" but then if you actually want to get anywhere you need some lemma to say that all X's have generators, or maybe even that one generator of X has property Y iff they all do. Either you prove these lemmas or you don't. If you don't (and there are going to be a couple of times with schemes where I propose not proving the lemmas just yet) then it really would be impossible to give any examples at all because the lemmas are somehow part of the infrastructure. So perhaps I interpreted @Assia Mahboubi 's comments in a similar way to you but then went on and thought more about the consequences of constructing an example in the situation I had in mind, and realised that I was some genuine lemmas in algebraic geometry away from being able to give any example at all.

view this post on Zulip Sean Leather (Mar 01 2018 at 09:40):

Makes sense. I was thinking in the first order, whereas you were at a higher order. Good thing you're the mathematician. :wink:

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:47):

Kenny and I just finished the definition of a scheme.

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:49):

https://github.com/kbuzzard/lean-stacks-project/blob/ed8a255cef466794d4d836ffa6ffc1093532fa4b/src/scheme.lean#L430

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:49):

It passes no basic tests whatsoever, other than "compiles" and "is mathematically correct".

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:52):

In particular, for any commutative ring R we can build an affine scheme Spec(R), but we have not yet proved that this object is a scheme.

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:52):

We are a couple of theorems away from this.

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:56):

[the issue is that a scheme is a space with a sheaf, locally isomorphic to an affine scheme, but this isomorphism is an isomorphism of spaces with presheaves of rings (a morphism of sheaves is by definition a morphism of the underlying presheaves) so we do not logically need to check that the presheaf of rings that we have defined on Spec(R) is a sheaf]

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 21:15):

Now for perfectoid spaces ;-)


Last updated: May 12 2021 at 04:19 UTC