We stand with Ukraine  

Mario Carneiro

Orcid: 0000-0002-0470-5249

Affiliations:
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Ohio State University, Department of Mathematics, Columbus OH, USA (former)


According to our database1, Mario Carneiro authored at least 18 papers between 2015 and 2025.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2025
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.
[BibTeX]
[DOI]
Magnus O. Myreen
,
Mario Carneiro
Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

Formalizing Colimits in 𝒞at.
[BibTeX]
[DOI]
Mario Carneiro
,
Emily Riehl
Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

2024
EmptyHexagonLean.
[BibTeX]
[DOI]
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.
[BibTeX]
[DOI]
Mario Carneiro
CoRR, 2024

Formal Verification of the Empty Hexagon Number.
[BibTeX]
[DOI]
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.
[BibTeX]
[DOI]
Mario Carneiro
,
Chad E. Brown
,
Josef Urban
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Reimplementing Mizar in Rust.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022
The Divergence of the Sum of Prime Reciprocals.
[BibTeX]
[DOI]
Mario Carneiro
Formaliz. Math., 2022

2021
A Flexible Proof Format for SAT Solver-Elaborator Communication.
[BibTeX]
[DOI]
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.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019
Metamath Zero: The Cartesian Theorem Prover.
[BibTeX]
[DOI]
Mario Carneiro
CoRR, 2019

Specifying verified x86 software from scratch.
[BibTeX]
[DOI]
Mario Carneiro
CoRR, 2019

Formalizing Computability Theory via Partial Recursive Functions.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Data Types as Quotients of Polynomial Functors.
[BibTeX]
[DOI]
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.
[BibTeX]
[DOI]
Mario Carneiro
J. Formaliz. Reason., 2016

Models for Metamath.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the Joint Proceedings of the FM4M, 2016

Formalization of the prime number theorem and Dirichlet's theorem.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the Joint Proceedings of the FM4M, 2016

2015
Arithmetic in Metamath, Case Study: Bertrand's Postulate.
[BibTeX]
[DOI]
Mario Carneiro
Proceedings of the CICM 2015, 2015


  Loading...