skip to content

Department of Pure Mathematics and Mathematical Statistics

Publications

Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization
J Bayer, M David, M Hassler, Y Matiyasevich, D Schleicher
(2025)
A Formal Proof of Complexity Bounds on Diophantine Equations
J Bayer, M David
(2025)
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
J Liu, X Lin, J Bayer, Y Dillies, W Jiang, X Liang, R Soletskyi, H Wang, Y Xie, B Xiong, Z Yang, J Zhang, L Zhi, J Li, Z Liu
(2025)
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
H Wang, M Unsal, X Lin, M Baksys, J Liu, MD Santos, F Sung, M Vinyes, Z Ying, Z Zhu, J Lu, HD Saxcé, B Bailey, C Song, C Xiao, D Zhang, E Zhang, F Pu, H Zhu, J Liu, J Bayer, J Michel, L Yu, L Dreyfus-Schmidt, L Tunstall, L Pagani, M Machado, P Bourigault, R Wang, S Polu, T Barroyer, W-D Li, Y Niu, Y Fleureau, Y Hu, Z Yu, Z Wang, Z Yang, Z Liu, J Li
(2025)
Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning
S Frieder, J Bayer, S Looi, J Loader, J Berner, KM Collins, A Juhász, F Ruehle, S Welleck, G Poesia, R-R Griffiths, A Weller, A Goyal, C Freer, T Lukasiewicz, T Gowers
(2024)
Mathematical Proof Between Generations.
J Bayer, C Benzmüller, K Buzzard, M David, L Lampert, Y Matiyasevich, L Paulsen, D Schleicher, B Stock, E Zelmanov
– Notices of the American Mathematical Society
(2024)
abs/2207.04779,
79
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
J Bayer, A Gonus, C Benzmüller, DS Scott
(2023)
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
J Bayer, A Gonus, C Benzmüller, DS Scott
(2023)
14101,
69
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
J Bayer, M David, A Pal, B Stock
(2021)
Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle
J Bayer, M David, A Pal, B Stock
(2019)
11617,
16
  • 1 of 2
  • >

Research Group

Combinatorics

Room

C0.04

Personal homepage