An introduction to theorem provers

Abstract: In this talk, we will introduce proof assistants, pieces of softwarethat formally verify mathematical proofs.Lean has a very extensivedatabase with mathematical results at the undergraduate level for-mally verified, and it is even used to verify new research. This hasseveral applications, including teaching, automatically verifying publi-cations, and even automated theorem proving. At the end of this talk,we will carry out a demo of Lean to show the basics and how you canget started.

Mathematics

Audience: advanced learners

Barcelona Mathematics Informal Seminar (SIMBa)

Series comments: SIMBa is a youth mathematics seminar organized by graduate students of the Barcelona area. It is aimed towards graduate and last course undergraduate students. Our goals are divulging the knowledge from different branches of mathematics for those interested and promote networking between the attendants.

This seminar is backed by the Faculty of Mathematics and Computer Science at Universitat de Barcelona, Faculty of Mathematics and Statistics at Universitat Politècnica de Catalunya, the Department of Mathematics from Universitat Autònoma de Barcelona, CRM, IMUB and BGSMath.