Re: [mizar] Compositions of regular matroids, Lean and Mizar

Hello,

This is an interesting topic.

Well, your suspicions are correct, you would not experience the same "technical difficulties". In the example given: the type `α` is irrelevant in the Mizar formalization, and thanks to Mizar's adjective system you could avoid casting types if you formalize the material correctly (a big "if").

I'll have to sleep on it, then try sketching out a formalization in Mizar to check that the adjective system works in our favor.

In my experience formalizing math in dependently-typed proof assistants, it does feel like I have to chant a small prayer to the gods of redundancy to assist me as I work. I don't have the same feeling when working with HOL or Mizar (or Isabelle).

Best,
Alex

On Mon, Jul 14, 2025 at 11:41 AM martin.dvorak _AT_ matfyz.cz <owner-mizar-forum@mizar.uwb.edu.pl> wrote:

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