Mario Carneiro
Mario Carneiro is a visiting researcher in computing science at Chalmers University of Technology. His research concerns the foundations and verification of proof systems. He started working with interactive theorem provers in 2013, first in Metamath and then in Lean, and he is a founder and maintainer of the Mathlib Lean library. His PhD at Carnegie Mellon introduced Metamath Zero, a minimalistic language that can verify the machine code of a proof checker for itself. In June 2025 he spoke at a Newton Institute seminar on the theory behind Lean, and in January 2026 he gave the WITS keynote on Lean4Lean.
- Works
- 26
- Citations
- 59
- h-index
- 6
Publication numbers from OpenAlex, as of 15 October 2026.
Timeline
-
2013
Formalizing mathematics in Metamath and Lean
He starts working with interactive theorem provers in 2013, first in Metamath and then in Lean. He is a founder and maintainer of the Mathlib Lean library.
-
August 2016
Formalizing the prime number theorem
He submits a formalization of the prime number theorem and Dirichlet's theorem to arXiv in August 2016.
-
October 2019
The Metamath Zero theorem prover
He submits Metamath Zero: The Cartesian Theorem Prover to arXiv in October 2019.
-
August 2022
A PhD under Jeremy Avigad
He completes a PhD in pure and applied logic at Carnegie Mellon in August 2022, advised by Jeremy Avigad. The thesis introduces Metamath Zero, a minimalistic language that can verify the machine code of a proof checker for itself.
-
2022–2024
A Hoskinson Center postdoc
His first position is a postdoctoral research fellowship at the Hoskinson Center at Carnegie Mellon University, held from 2022 to 2024.
-
June 2025
A talk on Lean's theory
He speaks at a Newton Institute seminar in June 2025, on the theory behind Lean.
-
January 2026
A keynote on Lean4Lean
He gives the keynote on Lean4Lean at the WITS 2026 workshop in January 2026.
-
As of October 2026
Visiting researcher at Chalmers
He is a visiting researcher in computing science at Chalmers University of Technology.
Sources and credits
Photo: We have no published photo of Mario Carneiro yet. Send us a free-licensed photo.
- Lean4Lean: Mechanizing the Metatheory of Lean (WITS 2026) - POPL 2026
- [1608.02029] Formalization of the prime number theorem and Dirichlet's theorem
- [1910.10703] Metamath Zero: The Cartesian Theorem Prover
- Jeremy Avigad's Home Page
- Pure and Applied Logic
- talks.cam : Lean Meta-theory: The Proofs behind the Proofs
- Mario Carneiro | Chalmers