Mario Carneiro

28 papers B 8C 1Journal 15Unranked 4
YearRankTypeTitle / Venue / Authors
2026 B conf
A Certifying Proof Assistant for Synthetic Mathematics in Lean.
CPP
Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey
2025 B conf
Formalizing Colimits in 𝒞at.
ITP
Mario Carneiro, Emily Riehl
2025 B conf
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.
ITP
Magnus O. Myreen, Mario Carneiro
2025 J jnl
GOL in GOL in HOL: Verified Circuits in Conway's Game of Life.
CoRR
Magnus O. Myreen, Mario Carneiro
2025 J jnl
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.
CoRR
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
2024 B conf
Formal Verification of the Empty Hexagon Number.
ITP
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
2024 J jnl
Formal Verification of the Empty Hexagon Number.
CoRR
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule
2024 J jnl
Lean4Lean: Towards a formalized metatheory for the Lean theorem prover.
CoRR
Mario Carneiro
2023 B conf
Automated Theorem Proving for Metamath.
ITP
Mario Carneiro, Chad E. Brown, Josef Urban
2023 B conf
Reimplementing Mizar in Rust.
ITP
Mario Carneiro
2023 J jnl
Reimplementing Mizar in Rust.
CoRR
Mario Carneiro
2022 J jnl
A Flexible Proof Format for SAT Solver-Elaborator Communication.
Log. Methods Comput. Sci.
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2022 J jnl
The Divergence of the Sum of Prime Reciprocals.
Formaliz. Math.
Mario Carneiro
2021 — conf
A Flexible Proof Format for SAT Solver-Elaborator Communication.
TACAS (1)
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2021 J jnl
A Flexible Proof Format for SAT Solver-Elaborator Communication.
CoRR
Seulkee Baek, Mario Carneiro, Marijn J. H. Heule
2020 C conf
Metamath Zero: Designing a Theorem Prover Prover.
CICM
Mario Carneiro
2019 B conf
Data Types as Quotients of Polynomial Functors.
ITP
Jeremy Avigad, Mario Carneiro, Simon Hudon
2019 B conf
Formalizing Computability Theory via Partial Recursive Functions.
ITP
Mario Carneiro
2019 J jnl
Metamath Zero: The Cartesian Theorem Prover.
CoRR
Mario Carneiro
2019 J jnl
Specifying verified x86 software from scratch.
CoRR
Mario Carneiro
2018 J jnl
Formalizing computability theory via partial recursive functions.
CoRR
Mario Carneiro
2016 J jnl
Conversion of HOL Light proofs into Metamath.
J. Formaliz. Reason.
Mario Carneiro
2016 — conf
Formalization of the prime number theorem and Dirichlet's theorem.
FM4M/MathUI/ThEdu/DP/WIP@CIKM
Mario Carneiro
2016 — conf
Models for Metamath.
FM4M/MathUI/ThEdu/DP/WIP@CIKM
Mario Carneiro
2016 J jnl
Models for Metamath.
CoRR
Mario Carneiro
2015 — conf
Arithmetic in Metamath, Case Study: Bertrand's Postulate.
CICM (Work in Progress)
Mario Carneiro
2015 J jnl
Arithmetic in Metamath, Case Study: Bertrand's Postulate.
CoRR
Mario Carneiro
2014 J jnl
Conversion of HOL Light proofs into Metamath.
CoRR
Mario Carneiro