5 citations · 8 across the 5 of their papers we have counts for
6 papers
A First Introduction to Isabelle/ML Metaprogramming: Automatic Estimation of Polynomial Degrees
Jonas Bayer, Anna Danilkin, Marco David +1
This article offers an introduction to metaprogramming in Isabelle/HOL for beginners, based on a running example for working with multivariate polynomials. The example is motivated…
Diophantine Equations over : Universal Bounds and Parallel Formalization
Jonas Bayer, Marco David, Malte Hassler +2
This paper explores multiple closely related themes: bounding the complexity of Diophantine equations over the integers and developing mathematical proofs in parallel with formal t…
A Formal Proof of Complexity Bounds on Diophantine Equations
Jonas Bayer, Marco David
We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory. Hilbert's Tenth Prob…
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Jonas Bayer, Aleksey Gonus, Christoph Benzmüller +1
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic…
Mathematical Proof Between Generations
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard +7
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This…
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
Jonas Bayer, Marco David, Abhik Pal +1
How difficult are interactive theorem provers to use? We respond by reviewing the formalization of Hilbert's tenth problem in Isabelle/HOL carried out by an undergraduate research…