Barcelona Fall Workshop on Number Theory II
Formal theorem proving with a view towards Diophantine equations
Ponentes
Sander R. Dahmen (VU Univ. Amsterdam)
Resumen
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.
Ficheros
No hay ficheros disponibles para descargar
Cuenta
Idiomas: