Mario Carneiro

According to our database, Mario Carneiro authored at least 20 papers between 2015 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2026

A Certifying Proof Assistant for Synthetic Mathematics in Lean.

Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.

Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng

CoRR, December, 2025

GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.

Magnus O. Myreen, Mario Carneiro

Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

Formalizing Colimits in 𝒞at.

Mario Carneiro, Emily Riehl

Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

2024

EmptyHexagonLean.

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule

Dataset, November, 2024

Lean4Lean: Towards a formalized metatheory for the Lean theorem prover.

Mario Carneiro

CoRR, 2024

Formal Verification of the Empty Hexagon Number.

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2023

Automated Theorem Proving for Metamath.

Mario Carneiro, Chad E. Brown, Josef Urban

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Reimplementing Mizar in Rust.

Mario Carneiro

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

The Divergence of the Sum of Prime Reciprocals.

Mario Carneiro

Formaliz. Math., 2022

2021

A Flexible Proof Format for SAT Solver-Elaborator Communication.

Seulkee Baek, Mario Carneiro, Marijn J. H. Heule

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

2020

Metamath Zero: Designing a Theorem Prover Prover.

Mario Carneiro

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019

Metamath Zero: The Cartesian Theorem Prover.

Mario Carneiro

CoRR, 2019

Specifying verified x86 software from scratch.

Mario Carneiro

CoRR, 2019

Formalizing Computability Theory via Partial Recursive Functions.

Mario Carneiro

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Data Types as Quotients of Polynomial Functors.

Jeremy Avigad, Mario Carneiro, Simon Hudon

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2016

Conversion of HOL Light proofs into Metamath.

Mario Carneiro

J. Formaliz. Reason., 2016

Models for Metamath.

Mario Carneiro

Proceedings of the Joint Proceedings of the FM4M, 2016

Formalization of the prime number theorem and Dirichlet's theorem.

Mario Carneiro

Proceedings of the Joint Proceedings of the FM4M, 2016

2015

Arithmetic in Metamath, Case Study: Bertrand's Postulate.

Mario Carneiro

Proceedings of the CICM 2015, 2015