| 2026 | CPP | A Certifying Proof Assistant for Synthetic Mathematics in Lean. | Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey |
| 2025 | ITP | Formalizing Colimits in 𝒞at. | Mario Carneiro, Emily Riehl |
| 2025 | ITP | GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. | Magnus O. Myreen, Mario Carneiro |
| 2024 | ITP | Formal Verification of the Empty Hexagon Number. | Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden R. Codel, Mario Carneiro, Marijn J. H. Heule |
| 2023 | ITP | Reimplementing Mizar in Rust. | Mario Carneiro |
| 2023 | ITP | Automated Theorem Proving for Metamath. | Mario Carneiro, Chad E. Brown, Josef Urban |
| 2021 | TACAS | A Flexible Proof Format for SAT Solver-Elaborator Communication. | Seulkee Baek, Mario Carneiro, Marijn J. H. Heule |
| 2019 | ITP | Data Types as Quotients of Polynomial Functors. | Jeremy Avigad, Mario Carneiro, Simon Hudon |
| 2019 | ITP | Formalizing Computability Theory via Partial Recursive Functions. | Mario Carneiro |
| 2016 | CIKM | Formalization of the prime number theorem and Dirichlet's theorem. | Mario Carneiro |
| 2016 | CIKM | Models for Metamath. | Mario Carneiro |