| 2026 | LeanArchitect: Automating Blueprint Generation for Humans and AI. | Thomas Zhu, Pietro Monticone, Sean Welleck, Jeremy Avigad |
| 2026 | Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL. | Fang Yan, Benot Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, Burkhart Wolff |
| 2026 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2026 | Certified Infinite Descent Criteria in Isabelle/HOL. | Jamie Wright, Liron Cohen, Reuben N. S. Rowe, Andrei Popescu |
| 2026 | Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean. | Eric Jonathan Wang, Elif skpl |
| 2026 | 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper). | Josef Urban |
| 2026 | Complex Bounded Operators in Isabelle/HOL. | Dominique Unruh, Jos Manuel Rodrguez Caballero |
| 2026 | Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk). | Dominique Unruh |
| 2026 | ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving. | Amitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri |
| 2026 | Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral. | Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda |
| 2026 | Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). | Aeacus Sheng, Wenda Li, Paul B. Jackson |
| 2026 | TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq. | Johann Rosain, Julie Cailler |
| 2026 | String Diagrams for Monoidal Categories, in Rocq. | Damien Pous |
| 2026 | Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages. | Reed Mullanix, Jacques Carette |
| 2026 | Lazy Proof Automation for Separation Logic. | Valentin Mikhalchuk, Vladimir Gladshtein, Ilya Sergey |
| 2026 | A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper). | Arend Mellendijk |
| 2026 | Feedback & Synthesis in LLM-Assisted Termination Proofs. | Zeke Medley, Panagiotis Manolios |
| 2026 | Functional Correctness of an Optimized Modular Inversion Algorithm. | Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Toms Vallejos Parada |
| 2026 | Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees. | Yiming Lin, Ian Kariniemi, Yao Li |
| 2026 | Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation. | Meven Lennon-Bertrand, Alexis Saurin |
| 2026 | Fractional Separation Logic in Isabelle LLVM. | Peter Lammich |
| 2026 | Enhancing Interactive Theorem Prover Error Messages with Hints. | Maria Khakimova, Sra Juhosov, Jaro S. Reinders, Jesper Cockx |
| 2026 | Formally Verified Liveness with Multiparty Session Types in Rocq. | Omer Keskin, Nobuko Yoshida, Rob van Glabbeek |
| 2026 | Verification of the Garsia-Wachs Algorithm. | Makoto Kanazawa |
| 2026 | Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language. | Vladimir Gladshtein, K. Rustan M. Leino |