is formal abstracts maintained

Stream: new members

[Huỳnh Trần Khanh]

it seems inactive as of now

[Huỳnh Trần Khanh]

but it gets mentioned often

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

Hopefully I just explained it.

[Rob Lewis]

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]

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

[Eric Wieser]

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]

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]

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]

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]

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]

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]

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]

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]

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/