Assia Mahboubi: Machine-Checked Mathematics
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.
