Zulip Chat Archive

Stream: new members

Topic: is formal abstracts maintained


Huỳnh Trần Khanh (Feb 24 2021 at 10:27):

it seems inactive as of now

Huỳnh Trần Khanh (Feb 24 2021 at 10:30):

but it gets mentioned often

Kevin Buzzard (Feb 24 2021 at 10:35):

There are Pittsburgh people here who can probably give you an update. My understanding is that Hales has spent some time thinking hard about controlled natural language because this is what he wants the language of his database to be. In the mean time we're hard at work here formalising all the _definitions_ which one needs in order to be able to state modern mathematical theorems in a theorem prover.

Eric Wieser (Feb 24 2021 at 10:55):

Mathlib seems to have a "roadmap" directory containing statements without proof - is there interest in growing it?

Kevin Buzzard (Feb 24 2021 at 10:57):

My understanding of that directory, based on a conversation I had with Reid at LT2020, was that these were situations where he was convinced that he had found the right framework for setting up and proving some results, but didn't have the time to fill out the details himself. He mentioned that it was occasionally miserable when he felt like he knew the best way to approach some area in Lean and then didn't get round to doing it and then saw people doing it in inferior ways, and this was an attempt to prevent this. Yury's recent comment seems to indicate that for paracompact spaces it has worked well.

Rob Lewis (Feb 24 2021 at 11:06):

I've been tempted to delete the roadmap directory because it's sat untouched for a year, without even an explanation of what it is or how it's supposed to be used...

Kevin Buzzard (Feb 24 2021 at 11:06):

Hopefully I just explained it.

Rob Lewis (Feb 24 2021 at 11:06):

If someone wants to actually explain, advertise, and expand it, that would be great, but it's kind of dead weight right now

Rob Lewis (Feb 24 2021 at 11:07):

I mean a readme, some mention on the website, etc

Eric Wieser (Feb 24 2021 at 12:48):

IMO the danger in a roadmap directory is that someone might work on something without ever knowing that progress was already made in the roadmap.

What would be the opinion on allowing todo'd statements directly in the modules where the proof would eventually live? It would make mathlib not sorry-free, but perhaps that doesn't matter as long as things like library_search don't suggest sorried lemmas, and a linter prevents them being tagged simp.

Kevin Buzzard (Feb 24 2021 at 12:51):

The roadmap was just an idea which Reid wanted to try because he had figured out the way to do e.g. paracompactness in Lean and was worried that someone would do it in a worse way. He could also have used some github issue or project, this was just an experiment. I would let him speak for himself but I've not seen him around for a while so I'm just saying what he told me in Pittsburgh last year. In this case I suspect he made sure that the usual suspects (Patrick, Yury etc) knew about his roadmap and when one of them finally got around to doing it, they could follow his roadmap, as we just saw; Yury even explicitly thanked Reid for doing it. At the time I wondered whether other people would use roadmaps in this way, but instead we seem to have picked up a couple more projects and no other roadmaps.

Kevin Buzzard (Feb 24 2021 at 12:53):

Johan had a roadmap for flatness which he didn't have time to deal with, and in that case I just urged him to PR the definition only, which is now I believe in mathlib. This is yet another approach to this sort of thing. Johan has understood the correct way to formalise the definition but hasn't had time to make the API. I have committed to giving a class on flatness in 2 weeks' time so probably I will make the API in about 10 days' time.

Kevin Buzzard (Feb 24 2021 at 12:53):

These have all been different ways of solving the same problem -- when a mathematician can see the basic structure of the way a subject should go in Lean but doesn't have time to prove all the lemmas themselves. It would be interesting to have a conversation about how to deal with this situation in general.

Kevin Buzzard (Feb 24 2021 at 12:54):

In some sense we also did it with schemes -- all we have for schemes is the definition, but this came from several years of thinking very hard about the correct definition (and several wrong turns, most of them made by me as I was learning about DTT and its consequences).

Kevin Buzzard (Feb 24 2021 at 12:58):

The most extreme example is category theory, where there are a very small number of people (Scott, Reid, Bhavik) who are beginning to understand the right way to put in a huge number of definitions into mathlib, and are slowly doing this. I think this is why Mario is so suspicious about the whole area -- he is far more used to formalising stuff like finset where after the definition there is an essentially self-evident list of 500 lemmas which need to be proved and if you're an expert like him then most of the proofs are one-liners. finset is a very different kind of definition to Scheme.

Kevin Buzzard (Feb 24 2021 at 13:04):

One can look at the category theory directory and dismiss it as just a huge number of definitions and some theorems which take a long time to compile, but this view overlooks the huge amount of work, mostly done by Scott, to actually make the definitions work at all in Lean -- there were all sorts of problems with universes and general infrastructure (Scott wrote many tactics in order to get his definitions usable -- one didn't have to do this with finset). There will be more of this. As I'm fond of pointing out, there are 11 definitions of a discrete valuation ring on Wikipedia, and I chose an appropriate one and then together with Johan and Rob an API has organically formed around it. But for schemes we are going to run into this again and again. We are going to have to engage with questions such as "what is the correct Lean definition for the mathematical predicate that a morphism of schemes is finitely presented" (because there are several equivalent definitions) and what will happen when a mathematician convinces themselves that they have the right definition, but no time to make the API? Conversely there are mathematicians popping up here who say "oh I see you have schemes, I'd like to prove a theorem about them" but they can't because newcomers are in no position to make good definitions. The roadmap definition was precisely this. Reid's work showed that his definition of paracompact_space was usable because he could see that his todos would not be completely horrible.

Kevin Buzzard (Feb 24 2021 at 13:05):

Simiarly Johan's definition of flat -- he knows that out of all the definitions in the literature, the one he formalised is the easiest one to work with in Lean so he knows that this should be the definition with which we do the API-building.

Alex J. Best (Feb 24 2021 at 16:40):

Kevin Buzzard said:

There are Pittsburgh people here who can probably give you an update. My understanding is that Hales has spent some time thinking hard about controlled natural language because this is what he wants the language of his database to be. In the mean time we're hard at work here formalising all the _definitions_ which one needs in order to be able to state modern mathematical theorems in a theorem prover.

In fact Hales is giving a talk at cmsa on this later today, https://cmsa.fas.harvard.edu/tech-in-math/


Last updated: Dec 20 2023 at 11:08 UTC