Barcelona Fall Workshop on Number Theory II

Formal theorem proving with a view towards Diophantine equations


Sander R. Dahmen (VU Univ. Amsterdam)


Proof assistants, such as Coq, Isabelle, or Lean, are software tools which assist in rigorously expressing mathematical statements and their proofs in a formal logical language. The mathematics that has been formalized this way ranges from purely theoretical results to algorithmic ones. We will discuss several such results, including recent joint work with Hölzl and Lewis on the formalization of the Cap Set Problem in Lean. We also turn to effective methods for solving Diophantine equations, and discuss the desirability and possibilities to formalize aspects of these.


No files available for download