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 (chensw915@gmail.com) and we can discuss this in detail. Look forward to your reply.
Kind regards,
Shuwei