The study of Diophantine equation has always been people's interest. Although such equations are in a very primitive form, finding its solution seems less intuitive, and people, for centuries, strives to formulate the general solution, and no one has yet successfully achieve such a task.
If one can find such general solution, or algorithm to find the solution, many mathematical problems will be solved, including Goldbach conjecture and some other twin prime problems.
David Hilbert, one of the most famous German mathematician in 20th century, raised a question about the general algorithm to find solution to Diophantine equation.
Yuri Matiyasevich, in the late 20th century, formulate the solution for Hilbert 10th problem. The result shows that such algorithm cannot exists.
The main proof basically discusses about the close relation between recursively enumerable set and exponential Diophantine equation.
In 2017, Yuri Matiyasevich visited Jacobs University Bremen and initiate a further research into Hilbert 10th problem, and I am grateful I could be part of the team.
With the booming of information technology, automatic theorem proving software greatly simplified the task of mathematical research, and we decided to use Isabelle, a theorem prover designed in Cambridge to support our project.
This blog post denote the starting of this project, and I will write more about Hilbert 10th problem in detail in the next few post.