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.
翻译：互动理论证明人如何难以使用?我们通过审查Jacobs University Bremen的本科研究小组在Jabbos University Bremen进行的Isabelle/HOL研究组对Hilbert在Isabelle/HOL第十个问题的正规化工作作出反应。我们争辩说,如我们的例子所示,证明助理人员对于初学者将数学正规化是可行的。为了让实地更便于使用,我们还调查了学习互动理论证明人时出现的障碍。我们广泛主张在数学研究和课程中更多地采用互动理论证明人。
相关内容
微信扫码咨询专知VIP会员