Next meeting

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

Rough agenda:

- Have a live Isabelle demo (Abhik volunteered in coordination with Marco and Scott)
- Split the proof into smaller pieces and organize smaller teams.
- Discuss an interesting related workshop (maybe suitable for submitting the resulting paper of this project) http://sketis.net/isabelle/isabelle-workshop-2018

## 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 3x^{2} − 2xy − y^{2}z − 7 = 0 has an integer solution: x = 1, y = 2, z = (− 2). By contrast, the Diophantine equation x^{2} + y^{2} + 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."