TL;DR
This paper demonstrates that interactive theorem provers like Isabelle are accessible for beginners through a case study on formalizing Hilbert's tenth problem, highlighting their potential in education and research.
Contribution
It provides a feasibility study showing beginners can formalize complex mathematics in Isabelle and surveys learning hurdles to promote wider adoption.
Findings
Beginners can successfully formalize complex mathematics in Isabelle.
Interactive theorem provers are feasible tools for educational purposes.
Barriers to learning Isabelle are identified and discussed.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
