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)

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. - Jonas Bayer; Alexey Gonus; Christoph Benzmüller; Dana S. Scott (CICM, 2023)

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. - Jonas Bayer; Aleksey Gonus; Christoph Benzmüller; Dana S. Scott (CoRR, 2023)

Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning. - Simon Frieder; Jonas Bayer; Katherine M. Collins; Julius Berner; Jacob Loader; András Juhász; Fabian Ruehle; Sean Welleck; Gabriel Poesia; Ryan-Rhys Griffiths; Adrian Weller; Anirudh Goyal; et al. (CoRR, 2024)

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)

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. - Haiming Wang; Mert Unsal; Xiaohan Lin; Mantas Baksys; Junqi Liu; Marco Dos Santos; Flood Sung; Marina Vinyes; Zhenzhe Ying; Zekai Zhu; Jianqiao Lu; Hugues de Saxcé; et al. (CoRR, 2025)

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics. - Junqi Liu; Xiaohan Lin; Jonas Bayer; Yael Dillies; Weijie Jiang; Xiaodan Liang; Roman Soletskyi; Haiming Wang; Yunzhou Xie; Beibei Xiong; Zhengfeng Yang; Jujian Zhang; et al. (CoRR, 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)