Computer-verified proofs: 48 hours in Rome

Two DinAmicI are among the organizers of the workshop Computer-verified proofs: 48 hours in Rome, to be held at the Department of Mathematics of University of Rome Tor Vergata on 24-26 January 2024.

Website: https://www.mat.uniroma2.it/butterley/formalisation/

The workshop concerns interactive proof assistants, programs that allow one to write and verify mathematical proofs. As such, the focus is on the Lean 4 language and its mathematical library.

For those who want an overview, several talks will be presented on major aspects of this emerging field. For those who want to go deeper, a series of workshop-style sessions will be offered, intended to give participants first-hand knowledge. The aim is to provide an introduction to this area for working mathematicians and advanced students in a variety of fields.

Participants are kindly asked to register.