| A flexible proof format for SAT solver-elaborator communication S Baek, M Carneiro, MJH Heule Logical Methods in Computer Science 18, 2022 | 30 | 2022 |
| Formalizing computability theory via partial recursive functions M Carneiro arXiv preprint arXiv:1810.08380, 2018 | 18 | 2018 |
| Metamath Zero: Designing a theorem prover prover M Carneiro Intelligent Computer Mathematics: 13th International Conference, CICM 2020 …, 2020 | 15 | 2020 |
| Data types as quotients of polynomial functors J Avigad, M Carneiro, S Hudon 10th International Conference on Interactive Theorem Proving (ITP 2019), 2019 | 11 | 2019 |
| Conversion of HOL Light proofs into Metamath M Carneiro arXiv preprint arXiv:1412.8091, 2014 | 8 | 2014 |
| A Lean formalization of Matiyasevi\v {c}'s Theorem M Carneiro arXiv preprint arXiv:1802.01795, 2018 | 7 | 2018 |
| Formalization of the prime number theorem and Dirichlet's theorem M Carneiro arXiv preprint arXiv:1608.02029, 2016 | 5 | 2016 |
| Specifying verified x86 software from scratch M Carneiro arXiv preprint arXiv:1907.01283, 2019 | 4 | 2019 |
| Metamath zero: The cartesian theorem prover M Carneiro arXiv preprint arXiv:1910.10703, 2019 | 3 | 2019 |
| Models for Metamath M Carneiro arXiv preprint arXiv:1601.07699, 2016 | 3 | 2016 |
| GCH implies AC, a Metamath Formalization M Carneiro arXiv preprint arXiv:1506.03533, 2015 | 3 | 2015 |
| The divergence of the sum of prime reciprocals M Carneiro Formalized Mathematics 30 (3), 209-210, 2022 | 2 | 2022 |
| The Lean 3 Mathematical Library (mathlib) M Carneiro URL: https://robertylewis. com/files/icms/Carneiro_mathlib. pdf, 2018 | 2 | 2018 |
| Lean4Lean: Towards a formalized metatheory for the Lean theorem prover M Carneiro arXiv preprint arXiv:2403.14064, 2024 | 1 | 2024 |
| Reimplementing Mizar in Rust M Carneiro arXiv preprint arXiv:2304.08391, 2023 | 1 | 2023 |
| Automated theorem proving for Metamath M Carneiro, CE Brown, J Urban 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023 | 1 | 2023 |
| Arithmetic in Metamath, Case Study: Bertrand's Postulate M Carneiro arXiv preprint arXiv:1503.02349, 2015 | 1 | 2015 |
| Formal Verification of the Empty Hexagon Number B Subercaseaux, W Nawrocki, J Gallicchio, C Codel, M Carneiro, ... arXiv preprint arXiv:2403.17370, 2024 | | 2024 |
| Arithmetic in Metamath M CARNEIRO | | 2015 |
| Definitions in Metamath M Carneiro | | |
