Hi, I'm Mario Carneiro!

I am a post-doc working in interactive theorem proving at Carnegie Mellon University.

I primarily work on the Lean theorem prover and the Metamath language, and I am the author of the Metamath Zero language. I have also done a lot of dabbling in many other languages and like to work on interaction between theorem proving languages such as HOL Light, Coq, Isabelle, and any others I can get my hands on.

Please feel free to get in touch!