Computer-verified proofs: 48 hours in Rome

[ICTP Math Section]

24-26 January 2024, we are having a mini event on Lean in Rome.

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

This short program concerns interactive proof assistants, programs that 
allow you to write and verify mathematical proofs. As such, we focus on 
the Lean language and its mathematical library.

For those who want an overview, we present several talks on major 
aspects of this emerging field. For those who want to go deeper, we 
offer a series of workshop style sessions 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.

We would be grateful if you could spread this information as widely as 
possible to anyone who might be interested. Do not hesitate to contact 
us for any question.

------------

-- 
Koutou Mabilo
ICTP Mathematics Group
Leonardo Da Vinci Building
Strada Costiera no. 11
34151 Trieste, Italy
Tel. no.: +39-040-2240455

For to be free is not merely to cast off one's chains, but to live in a way
that respects and enhances the freedom of others. Nelson Mandela