Computer-verified proofs: 48 hours in Rome

24-26 January 2024

A short program consisting of talks and workshop sessions focussed on Lean 4 and its mathematical library. We will explore diverse aspects of computer-verified proofs and digital mathematical libraries.

Speakers and schedule

Event team

Several robots discussing mathematics at the black board

Colloquium talks

Four talks on major topics related to formalization, computer-verified proofs and digital mathematical libraries. This includes the underlying ideas, concrete implementations and recent successes.

Workshop sessions

A series of hands-on sessions which will give participants first-hand knowledge using the Lean 4, its mathematical library and associated tools.

Audience

The event is accessible to mathematicians of all stages, anyone who is curious to start or continue exploring the field of computer-verified proofs, particularly with Lean.