| 2024 | A Formalization of All Notions in the Statement of a Theorem by Deligne. Michail Karatarakis |
| 2024 | A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving. Mohamed Abdelghany, Adnan Rashid, Sofiène Tahar |
| 2024 | A Logical Framework Perspective on Conservativity. Florian Rabe |
| 2024 | Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins |
| 2024 | Chaining Extensionality Lemmas in Lean's Mathlib. Eric Wieser |
| 2024 | Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts. Christian Steinfeldt, Helena Mihaljevic |
| 2024 | Formalizing Coppersmith's Method in Isabelle/HOL. Katherine Kosaian, Yong Kiam Tan, Kristin Yvonne Rozier |
| 2024 | Formalizing Finite Ramsey Theory in Lean 4. David E. Narváez, Cruise Song, Ningxin Zhang |
| 2024 | Formalizing Pick's Theorem in Isabelle/HOL. Sage Binder, Katherine Kosaian |
| 2024 | Generating Formally Verified Quantum Fourier Transform Algorithms. Patrick Brinich, Jeremy Johnson |
| 2024 | HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover. Nour Dekhil, Adnan Rashid, Sofiène Tahar |
| 2024 | Incorporating a Database of Graphs into a Proof Assistant. Andrej Bauer, Katja Bercic, Gauvain Devillez, Jure Taslak |
| 2024 | Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings Andrea Kohlhase, Laura Kovács |
| 2024 | Oruga: Implementation and Use of Representational Systems Theory. Daniel Raggi, Gem Stapleton, Aaron Stockdill, Grecia Garcia Garcia, Peter C.-H. Cheng, Mateja Jamnik |
| 2024 | Partial Proof Terms in the Study of Idealized Proof Search. José Espírito Santo, Ana Catarina Sousa |
| 2024 | Remote Verification System for Mizar Integrated with Emwiki. Toshiki Kai, Yuta Teruya, Kazuhisa Nakasho |
| 2024 | Reusing Learning Objects via Theory Morphisms. Michael Kohlhase, Marcel Schütz |
| 2024 | Solving Hard Mizar Problems with Instantiation and Strategy Invention. Jan Jakubuv, Mikolás Janota, Josef Urban |
| 2024 | Towards Semantic Markup of Mathematical Documents via User Interaction. Luka Vrecar, Joe B. Wells, Fairouz Kamareddine |
| 2024 | Transforming Optimization Problems into Disciplined Convex Programming Form. Ramon Fernández Mir, Paul B. Jackson, Siddharth Bhat, Andrés Goens, Tobias Grosser |
| 2024 | Using General Large Language Models to Classify Mathematical Documents. Patrick D. F. Ion, Stephen M. Watt |
| 2024 | Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations. Ruocheng Shan, Abdou Youssef |