Off topic

Stream: maths

[Lucian]

IMG_2030.jpeg
It’s like sorry but in a rigorous paper.

[Patrick Massot]

I think Remark 8.4.1.2 can be greatly generalized: there are way more things that can be obtained in a similar manner.

[Johan Commelin]

I don't think this informal-sorry is exceptional. There can be many other things to say about this particular paper, or the topic that it treats. But informal-sorry is a well established concept in the mathematical literature, which doesn't particularly need to be pointed out, I think.

[Adam Topaz]

I would say this is more of a proof by (approximate) rfl as opposed to sorry :)

[Antoine Chambert-Loir]

This is an example of a proof using sorry.
image.png

[Filippo A. E. Nuccio]

image.png
This one also, and it even gives a hint on what it takes to close the sorry.

[Kevin Buzzard]

In that last one you can use Gross' trick to reduce to weight 2 so it's OK :-)

[Antoine Chambert-Loir]

What is that trick? Multiply by another weight one form which has adequate congruence properties?

[Number Eighteen]

If a proof is clear, obvious or immediate, then this fact does not need to be said. Otherwise, a one sentence sketch or point to the key result in the recent literature cannot possibly consume such tremendous amount of time to write.

It will also help us subhuman dumb-dumbs with a limited command of the literature to learn more efficiently, and to make us better writers in the unlikely event that despite our clear and obvious lack of talent, we chance into academia.

Can we do that? No? Ok. How about a compromise, then. Since, as we've established, these phrases are "informal-sorry" elements, I suggest the authors replace all the "it's clear" and "it's obvious" with "I'm sorry".

[Kim Morrison]

I will buy a drink of your choice for the first person to post a paper to arXiv with by sorry after a theorem or lemma statement.

[Johan Commelin]

@Number Eighteen I think almost everyone on this zulip agrees that we wish all occurences of "informal-sorry" will be replaced by hyperlinks to a completely detailed proof.
Nevertheless, the current status quo is what it is, and pointing out that one particular author makes use of this convention is not fruitful, I think.

If a proof is clear, obvious or immediate, then this fact does not need to be said. Otherwise, a one sentence sketch or point to the key result in the recent literature cannot possibly consume such tremendous amount of time to write.

I don't agree with you. When your medium of communication is a stack of 2-dimensional pieces of paper, then you have to optimize for a certain audience. And that audience might want to be reassured that a certain fact is true. Knowing that the fact is true can be enough for them to figure out why the result is true.
A proof of that particular fact might not exist in the literature, and spelling out the details might be annoying and (key point) distracting from the flow of the text that you are writing.

[Johan Commelin]

Scott Morrison said:

I will buy a drink of your choice for the first person to post a paper to arXiv with by sorry after a theorem or lemma statement.

Bjorn Poonen already gave such a proof in his lecture at the Noether100 conference. I think he gave his talk after the Lean talk by Sophie Morel.

Are you sure that there are no examples yet of by sorry proofs in formalization papers posted to the arXiv?

[Mario Carneiro]

The paper I submitted to ITP yesterday contains theorems proved by sorry, although I didn't use the word sorry in the paper (I wrote "Conjecture N" instead). You can find sorry in the associated formalization though

[Edward van de Meent]

depends... i know of a paper which says instance : add_group Z := sorry -- implementation omitted, but i'm not sure that counts.

[Edward van de Meent]

(it's Use and abuse of instance parameters in the Lean mathematical library by Anne Baanen )

[Adam Topaz]

Does this count? https://arxiv.org/abs/2309.14870

[Number Eighteen]

Johan Commelin said:

Number Eighteen I think almost everyone on this zulip agrees that we wish all occurences of "informal-sorry" will be replaced by hyperlinks to a completely detailed proof.
Nevertheless, the current status quo is what it is, and pointing out that one particular author makes use of this convention is not fruitful, I think.

If a proof is clear, obvious or immediate, then this fact does not need to be said. Otherwise, a one sentence sketch or point to the key result in the recent literature cannot possibly consume such tremendous amount of time to write.

I don't agree with you. When your medium of communication is a stack of 2-dimensional pieces of paper, then you have to optimize for a certain audience. And that audience might want to be reassured that a certain fact is true. Knowing that the fact is true can be enough for them to figure out why the result is true.
A proof of that particular fact might not exist in the literature, and spelling out the details might be annoying and (key point) distracting from the flow of the text that you are writing.

When did I ask anyone to spell details? I literally said "one sentence sketch". I am saying, if you state something as a theorem, and the theorem is "clear", don't give a proof saying "it's clear". You already listed it as a theorem. If the audience "you are optimizing for" is assured by "clear", it is also assured by your stating this as a theorem.

[Johan Commelin]

Ok, I think I misunderstood you. So you are fine with theorems without proofs, but if there is something resembling a proof, then it shouldn't be "It's clear"?

[Adam Topaz]

Johan Commelin said:

Ok, I think I misunderstood you. So you are fine with theorems without proofs, but if there is something resembling a proof, then it shouldn't be "It's clear"?

I actually do this all the time.... but I use \begin{fact} ... \end{fact} for something that doesn't need a proof.

[Number Eighteen]

Johan Commelin said:

Ok, I think I misunderstood you. So you are fine with theorems without proofs, but if there is something resembling a proof, then it shouldn't be "It's clear"?

Yes.

[Mario Carneiro]

I ran into this issue while formatting my paper as well. If there is a theorem whose proof is obvious, it's structurally awkward to have "Theorem N" because then people will expect a proof and so you just have to put in a dummy line like "Proof: QED."

[Mario Carneiro]

I should have used "Fact N"

[Adam Topaz]

NB: I've been called out by referees about some of the things I declared as "fact" :)

[Mario Carneiro]

I wonder how many of the papers cited are doing it for this reason

[Mario Carneiro]

I mean, arguably lean is doing it too: you have to write sorry because theorem foo : Bla := is syntactically incorrect

[Mario Carneiro]

There is also a bit of information provided by the dummy line itself, since it differentiates "proof omitted" from "proof is immediate"

[Number Eighteen]

Mario Carneiro said:

There is also a bit of information provided by the dummy line itself, since it differentiates "proof omitted" from "proof is immediate"

If a proof is omitted but not immediate, one sentence should be used to explain why the proof is omitted and where to find it or how to assemble it.

[Mario Carneiro]

(this is presumably more of an issue in formalization papers since in a math paper I guess "proof omitted" doesn't fly)

[Mario Carneiro]

Number Eighteen said:

If a proof is omitted but not immediate, one sentence should be used to explain why the proof is omitted and where to find it or how to assemble it.

and in a formalization paper the answer to "where to find it" is obvious

[Number Eighteen]

Mario Carneiro said:

(this is presumably more of an issue in formalization papers since in a math paper I guess "proof omitted" doesn't fly)

I wish you were right :smiling_face_with_tear:

[Utensil Song]

image.png

I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.

I was trying to find the original copy, but just learned that it's eventually lost.

[Antoine Chambert-Loir]

Mario Carneiro said:

I ran into this issue while formatting my paper as well. If there is a theorem whose proof is obvious, it's structurally awkward to have "Theorem N" because then people will expect a proof and so you just have to put in a dummy line like "Proof: QED."

On the opposite, some German mathematician of beginning 20th century was of the opposite opinion. Everything should have a proof, he believed, even if that proof is just: “Beweis: Klar.”