Beginners' quest to formalize mathematics: a feasibility study in Isabelle

DOI10.1007/978-3-030-23250-4_2zbMath1428.68340arXiv2106.12351OpenAlexW2955358137MaRDI QIDQ2287895

Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal

Publication date: 22 January 2020

Full work available at URL: https://arxiv.org/abs/2106.12351

zbMATH Keywords

interactive theorem provingIsabelleformalized mathematicsHilbert's tenth problem

Mathematics Subject Classification ID

Decidability (number-theoretic aspects) (11U05) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

The DPRM Theorem in Isabelle (Short Paper).

Uses Software

• Coq
• Isabelle/HOL
• Django
• Archive Formal Proofs

This page was built for publication: Beginners' quest to formalize mathematics: a feasibility study in Isabelle