Publications

• 2025

• A Formal Proof of Complexity Bounds on Diophantine Equations

  Jonas Bayer, Marco David

  Interactive Theorem Proving · Conference paper

• Diophantine Equations over the integers: Universal Bounds and Parallel Formalization

  Jonas Bayer, Marco David, Malte Hassler, Yuri Matiyasevich, Dierk Schleicher

  Preprint

• 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é, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Longhui Yu, Léo Dreyfus-Schmidt, Lewis Tunstall, Luigi Pagani, Moreira Machado, Pauline Bourigault, Ran Wang, Stanislas Polu, Thibaut Barroyer, Wen-Ding Li, Yazhe Niu, Yann Fleureau, Yangyang Hu, Zhouliang Yu, Zihan Wang, Zhilin Yang, Zhengying Liu, Jia Li

  Preprint

• 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, Lihong Zhi, Jia Li, Zhengying Liu

  Preprint

• 2024

• Mathematical Proof Between Generations

  Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lampert, Yuri Matiyasevich, Lawrence Paulsen, Dierk Schleicher, Benedikt Stock, Efim Zelmanov

  Notices of the American Mathematical Society · Journal article

• 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, Thomas Lukasiewicz, Timothy Gowers

  Preprint

• 2023

• Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation

  Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott

  Conference on Intelligent Computer Mathematics · Conference paper

• Syntactic Similarity in human-oriented ATP

  Jonas Bayer

  Freie Universität Berlin · Thesis

• 2019

• Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle

  Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock

  Conference on Intelligent Computer Mathematics · Conference paper

• The DPRM Theorem in Isabelle

  Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, Dierk Schleicher

  Interactive Theorem Proving · Conference paper

• 2018

• Beeindruckende Mathematik-Erfolge im 53. Bundeswettbewerb ,Jugend forscht‘

  Jonas Bayer, Marco David, Simon Dubischar, Malte Haßler, Abhik Pal, Michael Schmalian, Benedikt Stock, Stephanie Schiemann

  Mitteilungen der Deutschen Mathematiker-Vereinigung · Journal article

• Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle

  Benedikt Stock, Abhik Pal, Maria Antonia Oprea, Yufei Liu, Malte Sophian Hassler, Simon Dubischar, Prabhat Devkota, Yiping Deng, Marco David, Bogdan Ciurezu, Jonas Bayer, Deepak Aryal

  EasyChair Preprints

This list is pulled from my ORCID record.