Dear Mizar users,
I am reaching out to you on behalf of the Seymour team (Martin Dvorak, Tristan Figueroa-Reid, Rida Hamadani, Byung-Hak Hwang, Evgenia Karunus, Vladimir Kolmogorov, Alex Meiburg, Peter Nelson, Mark Sandey, Ivan Sergeev).
https://github.com/Ivan-Sergeyev/seymour
We have finished a formally verified proof of the easy direction (composition direction) of the Seymour's theorem about regular matroids in Lean 4. We are going to submit a paper about the formalization to CPP 2026.
During the development, we repeatedly noticed that working in type theory was sometimes really cumbersome. As a result, I started to wonder if it would be easier to develop our project in a proof assistant based on set theory, such as Mizar. Let me illustrate one of the difficulties... When proving that "if two standard representations of the same matroid have the same base, then the standard representation matrices have the same support", we had a specific element of type `α` (the ambient type of all sets we work with) which we sometimes needed to cast as an element of the ground set `E` = the set of columns `Y` of the matrix that defines the given matroid and sometimes as an element of an independent set `I` and other times as an element of a support of a certain finitely-supported function. I was wondering whether it was "too much of an overhead" from using type theory.
Please let me know if you have any insight about whether these problems would disappear in Mizar and whether other problems specific to Mizar would be likely to arise. While we are not looking for reïmplementation of the entire project in Mizar, some other form of collaboration on our upcoming paper (or a different future project) is possible.
Best regards,
--
Martin Dvorak (he/him)
+436704091492
https://madvorak.github.io/
All dates are written in the international (ISO 8601) format YYYY-MM-DD.
All times are written in the Central European Summer Time (Vienna, Prague, Warsaw, Berlin, Paris, Madrid, Rome, …).