A Lean formalization of Matiyasevi\v{c}'s Theorem

Mario Carneiro

A Lean formalization of Matiyasevi\v{c}'s Theorem

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1802.01795 v1 pith:3HDSAGV3 submitted 2018-02-06 math.LO

Mario Carneiro This is my paper · ORCID

classification math.LO

keywords theoremformalizationleanmatiyasevipelldevelopmentdiophantineequation

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

abstract

In this paper, we present a formalization of Matiyasevi\v{c}'s theorem, which states that the power function is Diophantine, forming the last and hardest piece of the MRDP theorem of the unsolvability of Hilbert's 10th problem. The formalization is performed within the Lean theorem prover, and necessitated the development of a small number theory library, including in particular the solution to Pell's equation and properties of the Pell $x,y$ sequences.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization
math.NT 2025-06 conditional novelty 7.0 of 10 full

Every Diophantine set over the naturals has an integer representation with only 11 unknowns and degree below an explicit but huge bound.

Pith tools