Skip to end of metadata
Go to start of metadata


ToDos before winter break starts:

  • Add your availability during Intersession below! @everyone

For the winter break:

  • Figure out your way through Isabelle. Post comments to the Progress Blog whenever you work on Isabelle.
    • Share your knowledge whenever possible! If applicable, add what you learned to the Isabelle Cheat Sheet.
  • If relevant progress for the project has been made, push your files to the git repository so everyone has access. See Getting started with git.
  • Compile List of Isabelle Obstacles to ask the Isabelle Mailing List at

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 at Technische Universität München and 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.


Agenda Winter Break & Intersession

StatusOC  OC JanOC 

Offline: Jan 5-19

Otherwise in Bremen

OCOC Jan 15-18 (only)

Online from beginning of January onwards

OC on 7, 8 Jan

OC from Jan 15 onwards

Online from beginning of January onwards

OC Jan 21-26

OC Feb 3 onwards

most of the time in Bremen

school starts again Jan 8

online until 12 Jan

in Bremen until end of Jan

(OC = On Campus)


Progress Blog

All our Isabelle code is available in the currently private repository on

 RepresentativesMidterm progress reportCurrent Issues
Group Chapter 3Yufei, Benedikt3.1-3.3: basic definitions; first proof 
Group Chapter 4Marco, Abhik2.5-2.6: basic definitionsSynatx errors (sad)


Physical copy of this book available in the library.

  • No labels