Assia Mahboubi: Machine-Checked Mathematics

Datum objave: 9. 11. 2020
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 12. 11. 2020, ob 14:15, spletni seminar

Seminar se bo tokrat pridužil matematičnemu kolokviju.

Attention: we meet at a non-standard time on Thursday, 12. 11. 202 at 14:15. 

Assia Mahboubi, INRIA, Francija

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 

Abstract: 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.