Seymour project blueprint to arXiv

Stream: Seymour

[Cameron Rampell]

Hi everyone,

I'm preparing to upload the Seymour Project blueprint to arXiv as a single compiled document (via LeanBlueprint). Before doing so, I wanted to check with contributors regarding authorship on the arXiv submission.

Based on my understanding, the current contributors include @Ivan S. , @Martin Dvořák @Mark Sandey, and @Pietro Monticone, and I would of course include myself as well. If you’ve contributed to the blueprint and would like your name included on the arXiv submission, please feel free to opt in. If you would prefer not to be listed as an author, that’s also completely fine: just let me know.

I’ll give at least one week before proceeding so that everyone has time to respond. If you have any questions or concerns about the submission, feel free to comment here or message me privately.

Thanks!

[Martin Dvořák]

I agree with my name on the arXiv submission.

[Cameron Rampell]

I just finished a rough draft of the blueprint to upload; let me if there are any red flags to remove or things I should change/add.

print.pdf

[Martin Dvořák]

I suggest checking that all \uses in the metadata correspond to \ref in the prose, apart from the obvious exceptions (such as definitions referred to by the keyword no longer require referring to the number of the definition).

For example, Corollary 79 should refer to the five or six theorems whose corollary it is of. Here, I would simply say:
"Structural induction using Theorem X, (...), and Theorem Z."

In places where the blueprint says "Proof. See implementation in Lean." I don't mind if dependencies are not provided, tho I might be nice to see a list of lemmas that come to the proof even tho we don't elaborate on how they are used in the proof.

Alternatively, I would look into whether the dependency graph could be tweaked so that it contains the numbers of lemmas rather than their identifiers — then it could be included in the paper. Currently, the dependency graph would be useless in a PDF document even if the letters were large enough to be legible.

[Martin Dvořák]

If you want to be scrupulous, I would change Corollary 79 to "Any good matroid of finite rank is regular." and similarly in previous places, but it might be too much work, as for most of the time, we didn't care about infinite matroids in the blueprint. IIRC, @Ivan S. was writing most of the blueprint as if he had finite matroids everywhere, and then during formalization we noticed "hey, this lemma works for infinite matroids as well" or "hey, this theorem works for all matroids of finite rank, not only for finite matroids".

[Martin Dvořák]

I'm not saying that "does XYZ work for infinite matroids" has to be answered in the blueprint, but it is certainly beneficial that we discuss it in our paper (and similarly in my thesis).

[Martin Dvořák]

Upon rereading your Introduction, I have two further recommendations:

The present document is a blueprint for the formalization of this theory in the Lean proof

Here I would say "Lean 4" because it is the first occurrence of the word "Lean" in the text and, simultaneously, it will lead to a better spacing of the paragraph. All subsequent occurrences of "Lean" should stay "Lean" without a version, IMO.

which serves as a primary reference for the decomposition theory and the matrix-based approach

I don't know what "decomposition theory" means but I guess it isn't relevant for us. I guess you can say "matroid theory" in its place and the rest of the sentence will still work. Together:

"Our presentation of the structural theory of regular matroids closely follows the exposition and terminology of Truemper’s monograph [1], which serves as a primary reference for the matroid theory and the matrix-based approach adopted throughout this blueprint."

Additionally, since this paragraph is made of a single sentence, it might be nice to add a second sentence, saying something like that we thank Klaus Truemper for replying to our question.

[Cameron Rampell]

Alright, I added some of your suggestions; the only thing I didn't add in yet was the dependency graph, which I'll get to later if you think it'd still be helpful. From what you've said, though, it sounds like it's mostly good to go?

print.pdf

[Martin Dvořák]

"We thank Klaus Truemper for helpful correspondence regarding aspects of the decomposition framework."
->
"We thank Klaus Truemper for helpful correspondence about the regularity of the 3-sum."

[Martin Dvořák]

BTW, if you want to order authors by the size of their contribution to the blueprint, you should move yourself to the 2nd or 3rd position. Another option is to order them alphabetically.

[Martin Dvořák]

Otherwise LGTM, but wait for what other contributors think.

[Pietro Monticone]

Cameron Rampell said:

Alright, I added some of your suggestions; the only thing I didn't add in yet was the dependency graph, which I'll get to later if you think it'd still be helpful. From what you've said, though, it sounds like it's mostly good to go?

print.pdf

There are a few typos I’ve fixed in the repo but are still present in the print.pdf.

[Martin Dvořák]

Just these two words, right?
https://github.com/Ivan-Sergeyev/seymour/pull/194/files

[Pietro Monticone]

Yep

[Martin Dvořák]

Cameron Rampell said:

I didn't add in yet was the dependency graph

I personally wouldn't bother adapting the dependency graph. It was just an idea, which I see would be too hard to implement.

[Mark Sandey]

Definition 8 seems to be incomplete. It just says “Matrix made of 4 blocks (2x2).”

I’m not sure if this is intentional?

[Martin Dvořák]

Good catch! There should be a drawing of a block matrix.

[Martin Dvořák]

That said, the main purpose of writing Definition 8 was to create a node inside the Dependency graph.

[Cameron Rampell]

Great. I got rid of all of the typos, and since Definition 8 didn't seem to be used anywhere else (and there's no dependency graph), I just deleted it. I think I'll try submitting it to arXiv now.

[Cameron Rampell]

I need someone to endorse the submission to arXiv, since I haven't submitted any papers there before. Code is DDM4C6, which you enter at http://arxiv.org/auth/endorse.php.

[Martin Dvořák]

Cameron Rampell said:

Great. I got rid of all of the typos, and since Definition 8 didn't seem to be used anywhere else (and there's no dependency graph), I just deleted it. I think I'll try submitting it to arXiv now.

It is used in many places, but in the PDF definitions are usually used implicitly, so I don't mind it has been removed.

[Martin Dvořák]

Cameron Rampell said:

I need someone to endorse the submission to arXiv, since I haven't submitted any papers there before. Code is DDM4C6, which you enter at http://arxiv.org/auth/endorse.php.

It doesn't let me.
image.png

[Cameron Rampell]

That's unfortunate. Since it looks like you've only uploaded 3 papers, do you think you could upload the paper on my behalf?

print.pdf

[Martin Dvořák]

Can somebody else endorse you?

[Cameron Rampell]

I think it would be easier if you could just submit it. I need to find someone who has uploaded four papers related to combinatorics on arXiv to be endorsed, and I don't know anybody who specializes in combinatorics. However, since you already uploaded the pre-print for the official Seymour formalization paper, I think you should have automatic endorsement privileges in the combinatorics category.

[Martin Dvořák]

Sorry, I currently don't want additional responsibilities. You will find somebody to endorse you. If I understand correctly, they must be an author of 4 "math papers" in the specified time window, not necessarily "combinatorics papers".

[Byung-Hak Hwang]

Sorry for the late reply, I’m just catching up on this conversation.
As far as I understand, arXiv endorsement is about subject-area relevance, so it usually requires having a few papers in combinatorics. I haven’t endorsed anyone before, but I do have several papers in combinatorics, so I could try. If you’d like, I can attempt the endorsement using the code above.

[Byung-Hak Hwang]

One quick question: is the paper corresponding to this blueprint separate from the paper that will be resubmitted to a conference? And more generally, is it standard practice in Lean projects to put the blueprint itself on arXiv? I don’t have much experience with this, so I wanted to check.

[Cameron Rampell]

Byung-Hak Hwang said:

Sorry for the late reply, I’m just catching up on this conversation.
As far as I understand, arXiv endorsement is about subject-area relevance, so it usually requires having a few papers in combinatorics. I haven’t endorsed anyone before, but I do have several papers in combinatorics, so I could try. If you’d like, I can attempt the endorsement using the code above.

Thanks for offering. Fortunately, I already got endorsed from someone else, so now I'm just waiting for the submission to be approved by arXiv.

[Cameron Rampell]

Byung-Hak Hwang said:

One quick question: is the paper corresponding to this blueprint separate from the paper that will be resubmitted to a conference? And more generally, is it standard practice in Lean projects to put the blueprint itself on arXiv? I don’t have much experience with this, so I wanted to check.

Yes, they are separate papers. I asked Martin about submitting the paper and he referred me to the blueprint on arXiv for the Carleson project. I just needed to write an abstract and other small stuff to upload it.

[Byung-Hak Hwang]

Cameron Rampell 말함:

Yes, they are separate papers. I asked Martin about submitting the paper and he referred me to the blueprint on arXiv for the Carleson project. I just needed to write an abstract and other small stuff to upload it.

I got it. Thanks for letting me know.

[Martin Dvořák]

Byung-Hak Hwang said:

One quick question: is the paper corresponding to this blueprint separate from the paper that will be resubmitted to a conference?

Yes, it is a separate paper and it will never be submitted anywhere.

[Martin Dvořák]

Byung-Hak Hwang said:

And more generally, is it standard practice in Lean projects to put the blueprint itself on arXiv?

I don't think it is a standard practice. Nevertheless, I don't see any reason why not to do it. At the same time, I don't see any good reason why to do it.

[Martin Dvořák]

Perhaps it could be useful for people who want to reïmplement it in a different language?

[Byung-Hak Hwang]

Martin Dvořák 말함:

Perhaps it could be useful for people who want to reïmplement it in a different language?

I understand. Thanks :)