Abstract
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 group at Jacobs University Bremen. We argue that, as demonstrated by our example, proof assistants are feasible for beginners to formalize mathematics. With the aim to make the field more accessible, we also survey hurdles that arise when learning an interactive theorem prover. Broadly, we advocate for an increased adoption of interactive theorem provers in mathematical research and curricula.
Author supplied keywords
Cite
CITATION STYLE
Bayer, J., David, M., Pal, A., & Stock, B. (2019). Beginners’ Quest to Formalize Mathematics: A Feasibility Study in Isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11617 LNAI, pp. 16–27). Springer Verlag. https://doi.org/10.1007/978-3-030-23250-4_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
