Formalization of the MRDP theorem in the Mizar system

DOI10.2478/FORMA-2019-0020MaRDI QIDQ2337340zbMATH OpenOpenAlexWikidataFDO

Authors Karol Pąk

Publication date 19 November 2019

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/forma-2019-0020

zbMATH Keywords

Diophantine relationsHilbert's 10th problem

Mathematics Subject Classification ID

Counting solutions of Diophantine equations (11D45) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Diophantine sets. II
• Basic Diophantine relations
• Diophantine sets. Preliminaries
• The Matiyasevich theorem. Preliminaries
• A Note on Diophantine Representations

Cites work

• Basic Diophantine relations
• Diophantine sets. II
• Four decades of \textsc{Mizar}. Foreword
• Hilbert's Tenth Problem is Unsolvable
• scientific article; zbMATH DE number 1016911 (Why is no real title available?)
• Logical number theory I. An introduction
• Mizar: state-of-the-art and beyond
• Pell's equation
• The Matiyasevich theorem. Preliminaries
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(8)

• The Matiyasevich theorem. Preliminaries
• Diophantine sets. Preliminaries
• Prime representing polynomial
• Basic Diophantine relations
• Diophantine equations and provability in mathematics
• Hilbert's Tenth Problem in Coq
• The DPRM Theorem in Isabelle (Short Paper).
• A formal proof of complexity bounds on Diophantine equations

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Formalization of the MRDP theorem in the Mizar system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2337340)