theHigherGeometer on Nostr: A proof of the negative solution to Hilbert's Tenth Problem, by Matiyasevich ...
A proof of the negative solution to Hilbert's Tenth Problem, by Matiyasevich
https://www.mathtube.org/lecture/notes/hilberts-tenth-problem (83 pages, incl frontmatter).
This was the basis for a formal proof in Isabelle (one of several that were achieved at roughly the same time, in various proof assistants, namely Rocq [née Coq], Lean and Mizar, though some of these were apparently only partial)
https://www.isa-afp.org/entries/DPRM_Theorem.html
https://www.mathtube.org/lecture/notes/hilberts-tenth-problem (83 pages, incl frontmatter).
This was the basis for a formal proof in Isabelle (one of several that were achieved at roughly the same time, in various proof assistants, namely Rocq [née Coq], Lean and Mizar, though some of these were apparently only partial)
https://www.isa-afp.org/entries/DPRM_Theorem.html