ITP 2026 submission

Stream: Seymour

[Martin Dvořák]

Who wants to be responsible for the ITP 2026 submission?
It would involve the following:

• collect all texts for our paper
• format the paper in the LIPICS format
• shorten the paper to fit within the page limit
• become the corresponding author
• in case of acceptance, either go to the conference or find somebody to go there to present the paper

[Cameron Rampell]

I think I could do everything other than going to the conference in person. What do you mean by "collecting all texts for the paper"?

[Martin Dvořák]

If you take on all the other responsibilities, I will be happy to guarantee [[presenting the paper or finding who will do it] in case we get the spot].

[Martin Dvořák]

Collecting all texts means that if somebody writes their chapter elsewhere, you will have to insert it into the paper.

[Martin Dvořák]

The deadline for abstracts is today.
@Cameron Rampell
Got it firmly in your hands?

[Cameron Rampell]

Sorry, where exactly am I supposed to submit the abstract? I don't have the login code.

[Cameron Rampell]

I assume this is the abstract we are submitting, right?

Seymour's decomposition theorem is a hallmark result in matroid theory presenting a structural characterization of the class of regular matroids. Formalization of matroid theory faces many challenges, most importantly that only a limited number of notions and results have been implemented so far. In this work, we formalize the proof of the forward (composition) direction of Seymour's theorem for regular matroids. To this end, we develop a library in Lean 4 that implements definitions and results about totally unimodular matrices, vector matroids, their standard representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary matroids given by their standard representations. Using this framework, we formally state Seymour’s decomposition theorem and implement a formally verified proof of the composition direction in the setting where the matroids have finite rank and may have infinite ground sets.

[Cameron Rampell]

I just created a new account using my email.

[Cameron Rampell]

Just finished a first initial dummy submission with all the abstract, preliminary version of our final draft, and author names.

[Martin Dvořák]

Thank you for handling it!

[Martin Dvořák]

FYI, as one of the two maintainers of the repository (of whom only I am active), I retain the authority over what version of code will be submitted to ITP, but the contents of the paper are up to yall. I will try to influence the editing of the paper as little as possible.

[Martin Dvořák]

It eluded us then, but that's no matter — tomorrow we will run faster, stretch out our arms farther... And one fine morning...

So we beat on, boats against the current, borne back ceaselessly into the past.

[Martin Dvořák]

Adapting to the changing times, we would like to ask all authors to declare which parts of their code was produced with the aid of GenAI (LLMs).

Afaik none of the code was written by LLMs. Or has anybody used them in the Seymour project?

[Vladimir Kolmogorov]

How is it going with the submission? The deadline is in 3 days. Maybe, we can use overleaf?

[Vladimir Kolmogorov]

Also, should we have a zoom call to discuss the submission?

[Byung-Hak Hwang]

I checked the submission and noticed that Cameron Rampell is not listed among the authors in the PDF. In fact, it seems that the submission is simply the version on arXiv, without any updates.

[Byung-Hak Hwang]

I took a look at this paper (https://arxiv.org/pdf/2509.04922) and I think our main weaknesses compared to it are: 1) we don't really explain why we designed our implementation the way we did, 2) we don't address how our work fits with mathlib, and 3) there is no discussion of what we actually learned from the project. But, I think we have no enough time for revising the full structure of the paper.

[Cameron Rampell]

Byung-Hak Hwang said:

I checked the submission and noticed that Cameron Rampell is not listed among the authors in the PDF. In fact, it seems that the submission is simply the version on arXiv, without any updates.

Yes, it is a dummy submission so I could put something there to complete the submission. I will update it shortly when my code compiles, which I'm having trouble with.

[Martin Dvořák]

Does the template itself (without our text) compile?

[Cameron Rampell]

I think I got a preliminary version now:
main.pdf
One issue is that the submission is 23 pages long, which 7 pages over the page limit of 16. It would be helpful for anyone more experienced with this project to recommend sections to cut out. Otherwise, I'll just figure out which parts seem less important on my own.

[Cameron Rampell]

All submissions are expected to be accompanied by anonymised supplementary material containing verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used.

Also, for this, can I just attach the files from the Github repo?

[Martin Dvořák]

I'll send you an anonymized release version of the repository in a few hours.

[Vladimir Kolmogorov]

These are suggestions on what to cut (comments / feedback / alternative suggestions are very welcome).

=================

• Sec. 4.1: remove Lean definitions (it's just copying them from Mathlib, probably not so important for the submission)

Add sentence "We use the assumption that the matroid has a finite rank (``RankFinite'' in Mathlib). Note that the ground set is allowed to be infinite."

• Sec. 4.2:

change "Mathlib implements this definition as follows:"
to "We implement this definition as follows" and later remark
"Note that the definition of total unimodularity and lemma Matrix.isTotallyUnimodular_iff have been incorporated in Mathlib".

• Sec. 6: Replace "To capture this theoretical definition, ..." and subsequent text
  with

"To this end, we implemented the definition

def Matrix.toMatroid {α R : Type*} {X Y : Set α}
[DivisionRing R] (A : Matrix X Y R) :
Matroid α := sorry

Note although linear independence is defined over semirings R, in the definition above we need to assume that R is a DivisionRing,
otherwise the resulting structure would not satisfy the augmentation property of a matroid."

• Sec. 9,10,11:

start all of them with mathematical definitions of 1,2,3-sums (from the blueprint).
Then explain how we implement them (in the case of 1 and 2-sums; remove everything about 3-sums).

Can we have the latex source on overleaf or github, so that we can all edit it?

[Martin Dvořák]

Cameron Rampell said:

One issue is that the submission is 23 pages long, which 7 pages over the page limit of 16.

One of the problems is that you copied the CPP version, which was typeset in two columns. There are actually things to be done to shorten the paper without sacrificing any content. Note that the code snippets have many linebreak that were not present in the repository. Now when you typeset into one column, you can remove these linebreaks. At the same time, replace Matrix.exists_standardRepr_isBase_isTU by its full name (originally, it was shortened to "TU" in order to make the name fit into a line). Also, some of the explicit linebreaks in the text can be (and should be) removed. And finally, there should be some kind of switch that will hide the list of authors from the document, which is how it should be submitted for the peer review and it is also the page count that matters.

[Martin Dvořák]

Martin Dvořák said:

I'll send you an anonymized release version of the repository in a few hours.

seymour.zip

[Martin Dvořák]

In case you want to mention the size of our codebase, the total length of the implementation is 8728 lines.

[Cameron Rampell]

Sec. 4.1 (21 matroids.tex): Removed all 6 Lean code blocks (ExchangeProperty, Maximal, ExistsMaximalSubsetProperty, Matroid, IndepMatroid, RankFinite). Kept the mathematical description of matroids via base axioms. Added: "We use the assumption that the matroid has a finite rank (RankFinite in Mathlib). Note that the ground set is allowed to be infinite."

Sec. 4.2 (22 totally unimodular matrices.tex): Changed "Mathlib implements this definition as follows" to "We implement this definition as follows".
Added remark: "Note that the definition of total unimodularity and lemma Matrix.isTotallyUnimodular_iff have been incorporated in Mathlib."

Sec. 6 (30 vector matroids.tex): Replaced the detailed 3-step construction (IndepCols → toIndepMatroid → toMatroid) and augmentation/finitary discussion with just the Matrix.toMatroid definition and a note about DivisionRing being required for the augmentation property.

Sec. 9 (40 sum 1.tex): Added formal mathematical definition of 1-sum from blueprint. Condensed the three-level implementation explanation into one paragraph + the Matroid.IsSum1of code block.

Sec. 10 (41 sum 2.tex): Added formal mathematical definition of 2-sum from blueprint. Kept the matrix-level code, the diagram showing how matrices are decomposed, and the Matroid.IsSum2of predicate.

Sec. 11 (42 sum 3.tex): Kept only the mathematical definition (NiceArray matrix diagrams). Removed all implementation code (~200 lines of Set.drop, MatrixSum3, blocksToMatrixSum3, toBlockSummandₗ,
main.pdf
toMatrixDropUnionDrop, standardReprSum3, etc.).

[Vladimir Kolmogorov]

A couple of comments:

• remove authors from pdf (I think the submission should be anonymized)
• add information about # lines of code somewhere (in the conclusions)?

[Martin Dvořák]

After shortening the explanation of the 1-sum implementation, it isn't clear what this sentence refers to:
"The StandardRepr level converts the output matrix indices (...)"
As a bare minimum, you should refer to the full name of the definition.

[Martin Dvořák]

The same problem is in the 2-sum chapter. It isn't clear what the following sentence refers to:
"The StandardRepr level first slices (...)"

[Martin Dvořák]

@Tristan Figueroa-Reid Did you write the short section about R10? Right now, it would fit into the page limit.

[Martin Dvořák]

@Cameron Rampell Don't you want to include the images that illustrate from 1-, 2-, 3-sum mean for graphic matroids?

[Martin Dvořák]

Has anybody checked that the supplementary material on https://submissions.floc26.org/ contains what it should contain and that it compiles?

[Martin Dvořák]

We also split our code into an “implementation” (detailed definitions and lemmas) and a “presentation” (key results with Lean’s #guard_msgs checks), ensuring the proof is both modular and trustworthy.

This sentence smells fishy, but I don't have a quick fix.

[Martin Dvořák]

BTW did you change
"We would like to dedicate the paper to the memory of Klaus Truemper (...)"
to
"We dedicate this paper to Klaus Truemper (...)"
in Acknowledgements?

Perhaps none of them should be in the version for peer review (afaik no Acknowledgements should stay in the blinded version), but the change is strange. Maybe I am just too sentimental, but the second formulation sounds a bit insensitive to me.

[Cameron Rampell]

If I do that, it doesn't save any space (all author names are replaced with "Anonymous" in red). Is that okay?

[Cameron Rampell]

Martin Dvořák said:

BTW did you change
"We would like to dedicate the paper to the memory of Klaus Truemper (...)"
to
"We dedicate this paper to Klaus Truemper (...)"
in Acknowledgements?

Perhaps none of them should be in the version for peer review (afaik no Acknowledgements should stay in the blinded version), but the change is strange. Maybe I am just too sentimental, but the second formulation sounds a bit insensitive to me.

Sorry about that. I just trimmed off some words because it saved a line, and I found the meaning virtually equivalent. But we're well under 16 pages, so I can reinstate it if you want.

[Martin Dvořák]

Cameron Rampell said:

If I do that, it doesn't save any space (all author names are replaced with "Anonymous" in red). Is that okay?

In this case, the number of authors is not anonymized. However, if it is how the template works, so be it.

[Martin Dvořák]

Cameron Rampell said:

But we're well under 16 pages, so I can reinstate it if you want.

Isn't the blinded version without Acknowledgments?

[Martin Dvořák]

I told you Matrix.exists_standardRepr_isBase_isTU isn't the full name.
Matrix.exists_standardRepr_isBase_isTotallyUnimodular is the name of the lemma.

[Martin Dvořák]

Good way to check that you didn't make any mistake when editing the code snippets is to take the final version of the paper and copy the code snippet back into the repository but with recall instead of def/lemma/theorem and see if it compiles. You might need Type _ in place of Type* in universe-polymorphic declarations.

[Martin Dvořák]

Matroids-AFP or Wan2025

These things should be citations, right?

[Martin Dvořák]

Also, as one of the reviewers noticed, Matroid.IsRegular.isGood isn't the full name of the theorem.
Matroid.IsRegular.isGood_of_rankFinite is the full name of the theorem stating the hard direction.

[Martin Dvořák]

Our implementation was 8728 lines long.

I suppose "is" would be better than "was" here.

[Martin Dvořák]

image.png
The size of the spaces after the colons is hilarious. If you can't make it a normal space, I'd rather see no space after the colons in this particular sentence.

[Martin Dvořák]

Martin Dvořák said:

Has anybody checked that the supplementary material on https://submissions.floc26.org/ contains what it should contain and that it compiles?

Hello. Has anybody tried to compile the version of the code that has been submitted with the paper?!

[Cameron Rampell]

main.pdf
Here's the PDF that I think will be our final submission to ITP. If there are any red flags, let me know and I can fix it out – I am available until 10 PM PST.

[Cameron Rampell]

Logging off now; best of luck for the paper!

[Martin Dvořák]

The submission period is now over. Thank you @Cameron Rampell for handling it!

I am disappointed by how many of you ignored the revisions of our paper. As a result, I had to point out numerous issues myself, which made me exert much more influence on this submission than I intended. I hoped that everybody would express their views on what the paper should contain, and I am sorry that the result doesn't reflect the opinions of all of us. As a consequence, the paper is again mostly "the thing that Martin and Ivan wrote" even though I wanted to step back and let others take the wheel.

While I am pretty good at writing code, I am absolutely miserable at writing text. Had others written the text collaboratively and I provided only the polished version of the code, the result could have been much better than what we submitted.