Skip to end of metadata
Go to start of metadata

Next meeting

Wednesday November 8, 20:45 to 22:00.
Lecture Hall, Research 1.

Rough agenda:

  1. Have a live Isabelle demo (Abhik volunteered in coordination with Marco and Scott)
  2. Split the proof into smaller pieces and organize smaller teams.
  3. Discuss an interesting related workshop (maybe suitable for submitting the resulting paper of this project)

About Us

The main goal of the Hilbert-10 workgroup is to formalize Yuri Matiyasevich's proof of Hilbert's Tenth problem using the computer proof assistance language Isabelle (developed by the Technische Universität München and the University of Cambridge). The project is supervised by Prof. Dr. Yuri Matiyasevich (Steklov Institute of Mathematics at St.Petersburg), Prof. Dr. Dierk Schleicher (Jacobs University), and Bernhard Reinke (Jacobs University).

Hilbert's 10th Problem

"Hilbert's tenth problem is the tenth on the list of mathematical problems that the German mathematician David Hilbert posed in 1900. It is the challenge to provide a general algorithm which, for any given Diophantine equation (a polynomial equation with integer coefficients and a finite number of unknowns) can decide whether the equation has a solution with all unknowns taking integer values.

For example, the Diophantine equation 3x2 − 2xy − y2z − 7 = 0 has an integer solution: x = 1,   y = 2,   z = (− 2). By contrast, the Diophantine equation x2 + y2 + 1 = 0 has no such solution.

Hilbert's tenth problem has been solved, and it has a negative answer: such a general algorithm does not exist. This is the result of combined work of Martin Davis, Yuri Matiyasevich, Hilary Putnam and Julia Robinson which spans 21 years, with Yuri Matiyasevich completing the theorem in 1970. The theorem is now known as Matiyasevich's theorem or the MRDP theorem."

— from "Hilbert's 10th Problem", Wikipedia.


If you want to access the physical copy of this book, please talk to Marco David (until Nov 13th 2017).

Blog stream

The discussed paper is attached to the Papers page here: Y. Matiyasevich - On Hilbert's Tenth Problem (1) General Strategy In the initial phase of the project, our focus shall lie on Chapter 3, and implementing and proving lemmata therein. This will allow everyone to gain experience in Isabelle while simultaneously making progress. On Chapter 3 The visualization of the proof using e.g. matrices is for humans only and need not be formalized in Isabelle. Instead,…

Recently updated

  • No labels