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 database¹, Mario Carneiro authored at least 15 papers between 2015 and 2024.

Collaborative distances:

Dijkstra number² of four.
Erdős number³ of three.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Bibliography

2024

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

[BibT_eX]

[DOI]

Mario Carneiro

CoRR, 2024

Formal Verification of the Empty Hexagon Number.

[BibT_eX]

[DOI]

Bernardo Subercaseaux

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

2023

Automated Theorem Proving for Metamath.

[BibT_eX]

[DOI]

Mario Carneiro

Chad E. Brown

Josef Urban

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

Reimplementing Mizar in Rust.

[BibT_eX]

[DOI]

Mario Carneiro

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

2022

A Flexible Proof Format for SAT Solver-Elaborator Communication.

[BibT_eX]

[DOI]

Seulkee Baek

Mario Carneiro

Marijn J. H. Heule

Log. Methods Comput. Sci., 2022

The Divergence of the Sum of Prime Reciprocals.

[BibT_eX]

[DOI]

Mario Carneiro

Formaliz. Math., 2022

2020

Metamath Zero: Designing a Theorem Prover Prover.

[BibT_eX]

[DOI]

Mario Carneiro

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

2019

Metamath Zero: The Cartesian Theorem Prover.

[BibT_eX]

[DOI]

Mario Carneiro

CoRR, 2019

Specifying verified x86 software from scratch.

[BibT_eX]

[DOI]

Mario Carneiro

CoRR, 2019

Formalizing Computability Theory via Partial Recursive Functions.

[BibT_eX]

[DOI]

Mario Carneiro

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

Data Types as Quotients of Polynomial Functors.

[BibT_eX]

[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.

[BibT_eX]

[DOI]

Mario Carneiro

J. Formaliz. Reason., 2016

Models for Metamath.

[BibT_eX]

[DOI]

Mario Carneiro

Proceedings of the Joint Proceedings of the FM4M, 2016

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

[BibT_eX]

[DOI]

Mario Carneiro

Proceedings of the Joint Proceedings of the FM4M, 2016

2015

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

[BibT_eX]

[DOI]

Mario Carneiro

Proceedings of the CICM 2015, 2015

Mario Carneiro

Timeline

Legend:

Links

Online presence:

On csauthors.net:

Bibliography

Loading...