Re: Compositions of regular matroids, Lean and Mizar
paul young ykyw2018b _AT_ yahoo.com <[email protected]> Thu, 25 Sep 2025 04:22:07 +0000 (UTC)
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
------=_Part_341544_105380959.1758774127185
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
=20
martin.dvorak _AT_ matfyz.cz (<[email protected]>) =E5=
=9C=A8 2025=E5=B9=B47=E6=9C=8815=E6=97=A5=E6=98=9F=E6=9C=9F=E4=BA=8C =E4=B8=
=8A=E5=8D=8802:38:45 [GMT+8] =E5=AF=AB=E9=81=93=EF=BC=9A =20
=20
Dear Mizar users,
I am reaching out to you on behalf of the Seymour team (Martin Dvorak, Tris=
tan Figueroa-Reid, Rida Hamadani, Byung-Hak Hwang, Evgenia Karunus, Vladimi=
r 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 (compositi=
on 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 w=
as sometimes really cumbersome. As a result, I started to wonder if it woul=
d 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 bas=
e, then the standard representation matrices have the same support", we had=
a specific element of type `=CE=B1` (the ambient type of all sets we 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 e=
lement of a support of a certain finitely-supported function. I was wonderi=
ng 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 wou=
ld disappear in Mizar and whether other problems specific to Mizar would 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,
--=20
Martin Dvorak (he/him)+436704091492https://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, War=
saw, Berlin, Paris, Madrid, Rome, =E2=80=A6).
=20
------=_Part_341544_105380959.1758774127185
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
<html><head></head><body><div class=3D"ydp5677d593yahoo-style-wrap" style=
=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:16px=
;"><div></div>
<div><br></div><div><br></div>
=20
</div><div id=3D"yahoo_quoted_9264536682" class=3D"yahoo_quoted">
<div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
=20
<div>
martin.dvorak _AT_ matfyz.cz (<owner-mizar-forum=
@mizar.uwb.edu.pl>) =E5=9C=A8 2025=E5=B9=B47=E6=9C=8815=E6=97=A5=E6=98=
=9F=E6=9C=9F=E4=BA=8C =E4=B8=8A=E5=8D=8802:38:45 [GMT+8] =E5=AF=AB=E9=81=93=
=EF=BC=9A
</div>
<div><br></div>
<div><br></div>
=20
=20
<div><div id=3D"yiv1937757210"><div><div><span style=3D"bac=
kground-color:transparent;">Dear Mizar users,</span></div><div><br></div><d=
iv>I am reaching out to you on behalf of the Seymour team (Martin Dvorak, T=
ristan Figueroa-Reid, Rida Hamadani, Byung-Hak Hwang, Evgenia Karunus, Vlad=
imir Kolmogorov, Alex Meiburg, Peter Nelson, Mark Sandey, Ivan Sergeev).</d=
iv><div><span style=3D"background-color:transparent;"><br></span></div><div=
><span style=3D"background-color:transparent;">https://github.com/Ivan-Serg=
eyev/seymour</span></div><div><span style=3D"background-color:transparent;"=
><br></span></div><div><span style=3D"background-color:transparent;">We hav=
e finished a formally verified proof of the easy direction (composition dir=
ection) of the Seymour's theorem about regular matroids in Lean 4. We are g=
oing to submit a paper about the formalization to CPP 2026.</span></div><di=
v><br></div><div>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 ba=
sed 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 we work with) which we sometimes needed to cast as an element of t=
he ground set `E` =3D the set of columns `Y` of the matrix that defines the=
given matroid and sometimes as an element of an independent set `I` and ot=
her times as an element of a support of a certain finitely-supported functi=
on. I was wondering whether it was "too much of an overhead" from using typ=
e theory.</div><div><br></div><div>Please let me know if you have any insig=
ht about whether these problems would disappear in Mizar and whether other =
problems specific to Mizar would be likely to arise. While we are not looki=
ng for re=C3=AFmplementation of the entire project in Mizar, some other for=
m of collaboration on our upcoming paper (or a different future project) is=
possible.</div><div><br></div><div>Best regards,<br></div><br>-- <br>Marti=
n Dvorak (he/him)<div>+436704091492</div><div>https://madvorak.github.io/<b=
r></div><div><br></div><div>All dates are written in the international (ISO=
8601) format YYYY-MM-DD.</div><div>All times are written in the Central Eu=
ropean Summer Time (Vienna, Prague, Warsaw, Berlin, Paris, Madrid, Rome, =
=E2=80=A6).</div><br></div></div></div>
</div>
</div></body></html>
------=_Part_341544_105380959.1758774127185--