Introducing myself: Tetsuya Ishiu

Stream: new members

[Tetsuya Ishiu]

Hello! I’m Tetsuya Ishiu, an associate professor in the Department of Mathematics at Miami University. My main research areas are set theory and set-theoretic topology, but I’ve been interested in formal proofs for a long time. I used to use Coq, but started Lean a few years ago. 

I started a project to formalize ZFC in the first-order logic by using the Mathlib.ModelTheory. It is still in a very early stage (v0.0.0), but I published it at the following URL. 

https://github.com/ishiut/fo_zfc

I would appreciate any comments on it or anything else!

[Kenny Lau]

You might want to refer to #26804

[Tetsuya Ishiu]

Thank you for letting me know about #26804. This seems to cover a large part of what I have done (though it was a good training for me). I will check it and see if I can modify my project in line with yours.