Barcelona Fall Workshop on Number Theory II
Formal theorem proving with a view towards Diophantine equations
Presenters
Sander R. Dahmen (VU Univ. Amsterdam)
Abstract
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.
Files
No files available for download
Account
Languages: