Assia Mahboubi: Machine-Checked Mathematics

The digital era has transformed the practice of research in mathematics: typesetting, communication means, experimentation, and even, the very nature of proofs. The middle of the 20th century has seen the advent of proofs of theorems that rely on too intensive calculations to be perfomed "by hand". This usage of the computational power of computers to establish mathematical truths pervades a wide variety of mathematics: number theory, dynamical systems, combinatorics, etc. In these cases, issues related to the reliability of software permeate the assesment of mathematical rigor conducted at the time of peer-reviewing.

Proof assistants are pieces of software that allow to do mathematics by computer. More specifically, they are designed for the development of libraries of digitized and machine-checked mathematics, which may or may not include computational parts. In this talk, we will discuss the advantages and the perspectives of the formal verification of mathematical theorems.

 

The lecture will be given via Zoom:

Topic: Kolokvij Mahboubi Time: Nov 12, 2020 02:00 PM Europe/Ljubljana

Join Zoom Meeting https://uni-lj-si.zoom.us/j/91398575847?pwd=TjVmeDQ3ZGFvRExpZGNLQTNPMUgyQT09

Meeting ID: 913 9857 5847 Passcode: 736326

 

Vljudno vabljeni!

Primož Moravec