Zulip Chat Archive

Stream: new members

Topic: formal abstracts


view this post on Zulip Anthony Bordg (Jun 24 2020 at 13:15):

Tom Hales's Formal Abstracts project is not currently accepting contributions. Does Mathlib require formalizations with complete proofs or some kind of formal abstracts is acceptable?

view this post on Zulip Johan Commelin (Jun 24 2020 at 13:20):

There is the roadmap/ directory... but it's not really the same thing.

view this post on Zulip Johan Commelin (Jun 24 2020 at 13:20):

But it's the only place where some form of sorry is allowed.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:35):

I have been thinking about using the roadmap directory, adding definitions of things but no theorems.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:37):

We had plenty of "formal abstracts" in the perfectoid project for a long time (and some people warned us that this was a bad approach, but I think that they were being informed by computer science projects -- certainly the disaster stories I heard were computer science related).

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:37):

We had sorried definitions, and then at some point we only had sorried theorems, and then at some point we had a sorry-free repository.

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:38):

See #2016, if you start using the roadmap directory, please write something about what it's supposed to be and how people should use it!

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:39):

I suspect that part of the reason nothing has been added since the first commit is because it's not explained or mentioned anywhere.

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:43):

IMO it's not a place for arbitrary "formal abstracts." There are lots of ways to define a concept, not all of them suited for proving things. Something that appears in that directory should be a mathlib-appropriate sketch, in that if the details are filled in, it can go in the main library.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:44):

Out of interest, how would you feel about a PR which made a new file called, say, ring_theory.gorenstein which just contained a three-line definition of a predicate is_gorenstein on comm_ring, and contained no theorems at all?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:45):

I run into people who say "hey I want to do some MSc level commutative algebra in Lean" and then it turns out that getting the basic definitions right is hard, so they don't get to the fun part of proving the theorems.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:46):

I was wondering whether such a file, together with a bunch of comments and some references, and some suggested theorems, could go in the roadmap directory.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 13:46):

https://en.wikipedia.org/wiki/Gorenstein_ring

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:47):

How do I know you got the basic definition right if you didn't prove anything about it? How do you know? If you justify your definition with comments, it sounds fine for a roadmap. (I have no desire to be dictator of roadmaps btw.) I wouldn't want to see that in mathlib proper.

view this post on Zulip Anthony Bordg (Jun 24 2020 at 13:48):

Rob Lewis said:

IMO it's not a place for arbitrary "formal abstracts." There are lots of ways to define a concept, not all of them suited for proving things. Something that appears in that directory should be a mathlib-appropriate sketch, in that if the details are filled in, it can go in the main library.

What would be a math project where every detail is filled in but that can't go in the main library?

view this post on Zulip Anthony Bordg (Jun 24 2020 at 13:49):

Assuming the project follows the style guidelines.

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:53):

Anthony Bordg said:

What would be a math project where every detail is filled in but that can't go in the main library?

It's easy to define something in a non-idiomatic way that won't mesh well with the rest of the library. For a random example, if you're doing something with limits, it should be done using filters. A theory set up with a more specific notion of limit isn't wrong, but probably won't integrate well.

view this post on Zulip Anthony Bordg (Jun 24 2020 at 13:55):

Rob Lewis said:

Anthony Bordg said:

What would be a math project where every detail is filled in but that can't go in the main library?

It's easy to define something in a non-idiomatic way that won't mesh well with the rest of the library. For a random example, if you're doing something with limits, it should be done using filters. A theory set up with a more specific notion of limit isn't wrong, but probably won't integrate well.

I totally agree, but it's a general problem, not a roadmap-specific potential problem.

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:56):

It's much easier to tell if your development meshes with the rest of the library if you fill in the proofs though.

view this post on Zulip Anthony Bordg (Jun 24 2020 at 13:58):

Sorry to bother :grinning: , but what's the purpose of this roadmap repo then?

view this post on Zulip Rob Lewis (Jun 24 2020 at 13:59):

I don't know! Which is why I ask
Rob Lewis said:

See #2016, if you start using the roadmap directory, please write something about what it's supposed to be and how people should use it!

:)

view this post on Zulip Anthony Bordg (Jun 24 2020 at 14:03):

Sorry, I did not realize it was a question!

view this post on Zulip Rob Lewis (Jun 24 2020 at 14:05):

No worries. I should emphasize, these are just my opinions and I have no interest in dealing with the roadmap directory myself, so if someone takes charge with a different plan for it, that's fine.

view this post on Zulip Reid Barton (Jun 24 2020 at 14:07):

The roadmap PR got merged while it was still in progress, but roughly speaking my thoughts are that theorem statements work better than definitions; for definitions one should expect that they might need to be adjusted for better compatibility with mathlib (or for correctness!) but for sufficiently simple definitions it is possible to get it right on the first try.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:22):

Rob Lewis said:

How do I know you got the basic definition right if you didn't prove anything about it? How do you know? If you justify your definition with comments, it sounds fine for a roadmap. (I have no desire to be dictator of roadmaps btw.) I wouldn't want to see that in mathlib proper.

This is CS paranoia. I'm a mathematician, let's assume I got it right. Who cares if I got the definition wrong anyway? I can just fix it once the discovery is made by the lemma-makers. This "don't make definitions without proving theorems" attitude is stopping people who can't make definitions from proving theorems. If you don't want the definitions in ring_theory that's absolutely fine! But I would really like to be able to put them somewhere, so that people who don't know about out_params and all the other arcane rules about not extending things with fewer variables can still do something useful.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:24):

I am sitting on 30 definitions in ring theory. I have people who can start on the 1000 theorems later.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:25):

I am trying to figure out a way forward which makes it easier for people who know MSc level mathematics to be able to contribute by proving theorems which would be helpful for the development of algebra in mathlib. More and more of these people are appearing out of the woodwork. Look at the DVR thread. It's a farce. A poor student couldn't get the definition to compile and almost gave up completely.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:26):

I want to be better prepared next time around. That same student is now happily proving theorems about DVRs.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:28):

There is general resistance to a top-down approach from the CS community, and Assia told me some nightmare story about some key wrong definition which cost a lot of time. But we tried a top down approach in the perfectoid project and it worked fine.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:28):

We went a little way down and then built up from the bottom and met in the middle.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:29):

The "little way down" was pretty much exactly what I am envisioning a formal abstract to be.

view this post on Zulip Sebastien Gouezel (Jun 24 2020 at 14:34):

I would be happy to see definitions-only PRs to mathlib if there are no sorries, if the PR review is even more thorough than usual (say, at least two different persons say they are happy with the definition), and if the PRs are short (i.e., better 10 PRs with 10 definitions than one PR with 10 definitions).

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:38):

I have been thinking about this because of pushing commutative algebra forwards. One big problem is that on the Wikipedia page for DVR they literally give ten definitions. How is a beginner going to know where to start?

view this post on Zulip Anthony Bordg (Jun 24 2020 at 14:41):

Sebastien Gouezel said:

I would be happy to see definitions-only PRs to mathlib if there are no sorries, if the PR review is even more thorough than usual (say, at least two different persons say they are happy with the definition), and if the PRs are short (i.e., better 10 PRs with 10 definitions than one PR with 10 definitions).

What about PRs in the roadmap directory? Will a PR with definitions and sketches of proofs be thoroughly reviewed? Such feedback would be very valuable or even critical for the top-down approach advertized by Kevin.

view this post on Zulip Sebastien Gouezel (Jun 24 2020 at 14:48):

Anthony Bordg said:

What about PRs in the roadmap directory?

I don't know either what roadmaps are for, and how such PRs would be handled. We need to invent some rules!

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 14:54):

In a long offline chat with Rob he persuaded me to put theoremless definitions in a separate repo.

view this post on Zulip Reid Barton (Jun 24 2020 at 15:04):

offline??

view this post on Zulip Johan Commelin (Jun 24 2020 at 15:09):

I guess off "this" line

view this post on Zulip Patrick Massot (Jun 24 2020 at 15:15):

I think he means "in the old world we used to have".

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 15:31):

Oh I meant in a bunch of private messages. I'd never heard this "offline" word before when I went to maths talks. In CS talks they use it all the time -- someone asks a question and the answer is "I can explain all this to you offline"

view this post on Zulip Scott Morrison (Jun 25 2020 at 03:35):

I think "definitions + sorried theorems" should be the minimum bar for roadmap/. Really though it should have some comments explaining the idea of the proof (not necessary even a math sketch --- even something saying "you should be able to prove this putting together existing results in XXX/YYY.lean).

view this post on Zulip Scott Morrison (Jun 25 2020 at 03:37):

I think we generally really need to explore the possibility that new contributors to mathlib don't need to start with a blank file. We want better mechanisms for divvying up the design / definition writing / theorem formulation / proofs amongst multiple people. Let's see if roadmap/ can do this.

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 17:24):

Scott Morrison said:

I think we generally really need to explore the possibility that new contributors to mathlib don't need to start with a blank file. We want better mechanisms for divvying up the design / definition writing / theorem formulation / proofs amongst multiple people. Let's see if roadmap/ can do this.

As a soon new contributor, I approve


Last updated: May 18 2021 at 17:44 UTC