Formalization of math theorems in Mizar

Dear colleagues,

This is Shuwei Chen, an associate professor at Southwest Jiaotong
University. My team is currently working on automated theorem proving and
found that Mizar provides a well-organized mathematical library that covers
a wide range of mathematical domains.

What we are trying to do is to prove some open mathematical problems using
our ATP prover, and verify the proof with the help of Mizar verifier and
submit it to Mizar library if got accepted. As the first step, we need to
formalize the corresponding math problems, preferable in Mizar language,
before feeding it to the ATP prover. As we are not familiar with Mizar
language, we are looking for the help from Mizar users to transform some
open math problems into Mizar language. Your work is much appreciated, and
this could benefit both sides. If you are interested, please do not
hesitate to contact me ([email protected]) and we can discuss this
in detail. Look forward to your reply.

Kind regards,

Shuwei