The DPRM Theorem in Isabelle (Short Paper). - Jonas Bayer; Marco David; Abhik Pal; Benedikt Stock; Dierk Schleicher (ITP, 2019)

Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle. - Jonas Bayer; Marco David; Abhik Pal; Benedikt Stock (CICM, 2019)

Digit Expansions. - Jonas Bayer; Marco David; Abhik Pal; Benedikt Stock (Arch. Formal Proofs, 2022)

Diophantine Equations and the DPRM Theorem. - Jonas Bayer; Marco David; Benedikt Stock; Abhik Pal; Yuri V. Matiyasevich; Dierk Schleicher (Arch. Formal Proofs, 2022)

Mathematical Proof Between Generations. - Jonas Bayer; Christoph Benzmüller; Kevin Buzzard; Marco David; Leslie Lamport; Yuri V. Matiyasevich; Lawrence C. Paulson; Dierk Schleicher; Benedikt Stock; Efim I. Zelmanov (CoRR, 2022)

Symplectic learning for Hamiltonian neural networks. - Marco David; Florian Méhats (J. Comput. Phys., 2023)

Universal Pairs for Diophantine Equations. - Marco David; Théo André; Mathis Bouverot-Dupuis; Eva Brenner; Loïc Chevalier; Anna Danilkin; Charlotte Dorneich; Kevin Lee; Xavier Pigé; Timothé Ringeard; Quentin Vermande; Paul Wang; et al. (Arch. Formal Proofs, 2025)

A Formal Proof of Complexity Bounds on Diophantine Equations. - Jonas Bayer; Marco David (CoRR, 2025)

Diophantine Equations over ℤ: Universal Bounds and Parallel Formalization. - Jonas Bayer; Marco David; Malte Hassler; Yuri V. Matiyasevich; Dierk Schleicher (CoRR, 2025)