Arithmetic in Metamath, Case Study: Bertrand's Postulate. - Mario Carneiro (CICM (Work in Progress), 2015)

Formalization of the prime number theorem and Dirichlet's theorem. - Mario Carneiro (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Models for Metamath. - Mario Carneiro (FM4M/MathUI/ThEdu/DP/WIP@CIKM, 2016)

Conversion of HOL Light proofs into Metamath. - Mario Carneiro (J. Formaliz. Reason., 2016)

Data Types as Quotients of Polynomial Functors. - Jeremy Avigad; Mario Carneiro; Simon Hudon (ITP, 2019)

Formalizing Computability Theory via Partial Recursive Functions. - Mario Carneiro (ITP, 2019)

Specifying verified x86 software from scratch. - Mario Carneiro (CoRR, 2019)

Metamath Zero: The Cartesian Theorem Prover. - Mario Carneiro (CoRR, 2019)

Metamath Zero: Designing a Theorem Prover Prover. - Mario Carneiro (CICM, 2020)

The Divergence of the Sum of Prime Reciprocals. - Mario Carneiro (Formaliz. Math., 2022)

A Flexible Proof Format for SAT Solver-Elaborator Communication. - Seulkee Baek; Mario Carneiro; Marijn J. H. Heule (Log. Methods Comput. Sci., 2022)

Reimplementing Mizar in Rust. - Mario Carneiro (ITP, 2023)

Automated Theorem Proving for Metamath. - Mario Carneiro; Chad E. Brown; Josef Urban (ITP, 2023)

Formal Verification of the Empty Hexagon Number. - Bernardo Subercaseaux; Wojciech Nawrocki; James Gallicchio; Cayden R. Codel; Mario Carneiro; Marijn J. H. Heule (ITP, 2024)

Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. - Mario Carneiro (CoRR, 2024)

EmptyHexagonLean. - Bernardo Subercaseaux; Wojciech Nawrocki; James Gallicchio; Cayden R. Codel; Mario Carneiro; Marijn J. H. Heule (DROPS Artifacts, 2024)

GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. - Magnus O. Myreen; Mario Carneiro (CoRR, 2025)