Barcelona Fall Workshop on Number Theory II
Formal theorem proving with a view towards Diophantine equations
Ponents
Sander R. Dahmen (VU Univ. Amsterdam)
Resum
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.
Fitxers
No hi ha fitxers per descarregar
Compte
Llengües: