Re: Compositions of regular matroids, Lean and Mizar

--000000000000d6dec50639ed9183
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

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  `=CE=B1` is irrel=
evant
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=E2=80=AFAM martin.dvorak _AT_ matfyz.cz <
[email protected]> 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 Sergee=
v).
>
> 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 i=
n
> Lean 4. We are going to submit a paper about the formalization to CPP 202=
6.
>
> 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 th=
e
> 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 the
> 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
> 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 wou=
ld
> 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).
>
>

--000000000000d6dec50639ed9183
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Hello,<br><br>This is an interesting topic.<br><br>Well, y=
our suspicions=C2=A0are correct, you would not experience the same &quot;te=
chnical difficulties&quot;. In the example given: the type

=C2=A0`=CE=B1` is irrelevant in the Mizar formalization, and thanks to Miza=
r&#39;s adjective system you could avoid casting types <i>if</i> you formal=
ize the material correctly (a big &quot;if&quot;).<br><br>I&#39;ll have to =
sleep on it, then try sketching out a formalization in Mizar to=C2=A0check =
that the adjective system works in=C2=A0our favor.<br><br>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 w=
ork. I don&#39;t have the same feeling when working with HOL or Mizar (or I=
sabelle).<br><br>Best,<br>Alex=C2=A0</div><br><div class=3D"gmail_quote gma=
il_quote_container"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Jul 14, 2=
025 at 11:41=E2=80=AFAM martin.dvorak _AT_ <a href=3D"http://matfyz.cz">mat=
fyz.cz</a> &lt;<a href=3D"mailto:[email protected]">owner-=
[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"g=
mail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204=
,204,204);padding-left:1ex"><div><div><span style=3D"background-color:trans=
parent">Dear Mizar users,</span></div><div><br></div><div>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, Ale=
x Meiburg, Peter Nelson, Mark Sandey, Ivan Sergeev).</div><div><span style=
=3D"background-color:transparent"><br></span></div><div><span style=3D"back=
ground-color:transparent"><a href=3D"https://github.com/Ivan-Sergeyev/seymo=
ur" target=3D"_blank">https://github.com/Ivan-Sergeyev/seymour</a></span></=
div><div><span style=3D"background-color:transparent"><br></span></div><div=
><span style=3D"background-color:transparent">We have finished a formally v=
erified proof of the easy direction (composition direction) of the Seymour&=
#39;s theorem about regular matroids in Lean 4. We are going to submit a pa=
per about the formalization to CPP 2026.</span></div><div><br></div><div>Du=
ring 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 th=
at &quot;if two standard representations of the same matroid have the same =
base, then the standard representation matrices have the same support&quot;=
, 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 ma=
troid 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 &quot;too much of an overhead&quot; from using ty=
pe theory.</div><div><br></div><div>Please let me know if you have any insi=
ght about whether these problems would disappear in Mizar and whether other=
 problems specific to Mizar would be likely to arise. While we are not look=
ing for re=C3=AFmplementation of the entire project in Mizar, some other fo=
rm of collaboration on our upcoming paper (or a different future project) i=
s possible.</div><div><br></div><div>Best regards,<br></div><br>-- <br>Mart=
in Dvorak (he/him)<div>+436704091492</div><div><a href=3D"https://madvorak.=
github.io/" target=3D"_blank">https://madvorak.github.io/</a><br></div><div=
><br></div><div>All dates are written in the international (ISO 8601) forma=
t YYYY-MM-DD.</div><div>All times are written in the Central European Summe=
r Time (Vienna, Prague, Warsaw, Berlin, Paris, Madrid, Rome, =E2=80=A6).</d=
iv><br></div></blockquote></div>

--000000000000d6dec50639ed9183--