formal abstracts

Stream: new members

[Anthony Bordg]

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?

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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).

[Kevin Buzzard]

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.

[Rob Lewis]

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!

[Rob Lewis]

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

[Rob Lewis]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Rob Lewis]

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.

[Anthony Bordg]

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?

[Anthony Bordg]

Assuming the project follows the style guidelines.

[Rob Lewis]

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.

[Anthony Bordg]

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.

[Rob Lewis]

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

[Anthony Bordg]

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

[Rob Lewis]

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!

:)

[Anthony Bordg]

Sorry, I did not realize it was a question!

[Rob Lewis]

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.

[Reid Barton]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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).

[Kevin Buzzard]

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?

[Anthony Bordg]

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.

[Sebastien Gouezel]

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!

[Kevin Buzzard]

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

[Reid Barton]

offline??

[Johan Commelin]

I guess off "this" line

[Patrick Massot]

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

[Kevin Buzzard]

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"

[Scott Morrison]

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).

[Scott Morrison]

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.

[Anatole Dedecker]

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