Compositions of regular matroids, Lean and Mizar
martin.dvorak _AT_ matfyz.cz <[email protected]> Mon, 14 Jul 2025 20:36:47 +0200 (CEST)
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <AWc.MQCd.68c}q8{8P9S.1eTKu}@seznam.cz> |
--=_31f9f5360113b528407fd277=d0983577-816d-5cd4-a63d-714ea96ad4ff_= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable 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 `=CE=B1` (the ambient type of all sets w= e work with) which we sometimes needed to cast as an element of the ground set `E= ` =3D the set of columns `Y` of the matrix that defines the given matroid an= d 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 woul= d be likely to arise. While we are not looking for re=C3=AFmplementation 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, =E2=80=A6). --=_31f9f5360113b528407fd277=d0983577-816d-5cd4-a63d-714ea96ad4ff_= Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <html><body><div><span style=3D"background-color:transparent">Dear Mizar u= sers,</span></div><div><br></div><div>I am reaching out to you on behalf o= f the Seymour team (Martin Dvorak, Tristan Figueroa-Reid, Rida Hamadani, B= yung-Hak Hwang, Evgenia Karunus, Vladimir Kolmogorov, Alex Meiburg, Peter = Nelson, Mark Sandey, Ivan Sergeev).</div><div><span style=3D"background-co= lor:transparent"><br></span></div><div><span style=3D"background-color:tra= nsparent">https://github.com/Ivan-Sergeyev/seymour</span></div><div><span = style=3D"background-color:transparent"><br></span></div><div><span style= =3D"background-color:transparent">We have finished a formally verified pro= of 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.</span></div><div><br></div><div>During the dev= elopment, 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 M= izar. Let me illustrate one of the difficulties... When proving that "if t= wo standard representations of the same matroid have the same base, then t= he standard representation matrices have the same support", we had a speci= fic element of type `=CE=B1` (the ambient type of all sets we work with) w= hich we sometimes needed to cast as an element of the ground set `E` =3D t= he set of columns `Y` of the matrix that defines the given matroid and som= etimes as an element of an independent set `I` and other times as an eleme= nt of a support of a certain finitely-supported function. I was wondering = whether it was "too much of an overhead" from using type theory.</div><div= ><br></div><div>Please let me know if you have any insight about whether t= hese problems would disappear in Mizar and whether other problems specific= to Mizar would be likely to arise. While we are not looking for re=C3=AFm= plementation of the entire project in Mizar, some other form of collaborat= ion on our upcoming paper (or a different future project) is possible.</di= v><div><br></div><div>Best regards,<br></div><br>-- <br>Martin Dvorak (he/= him)<div>+436704091492</div><div>https://madvorak.github.io/<br></div><div= ><br></div><div>All dates are written in the international (ISO 8601) form= at YYYY-MM-DD.</div><div>All times are written in the Central European Sum= mer Time (Vienna, Prague, Warsaw, Berlin, Paris, Madrid, Rome, =E2=80=A6).= </div><br></body></html> --=_31f9f5360113b528407fd277=d0983577-816d-5cd4-a63d-714ea96ad4ff_=--