FAU MoD Lecture Series. Special November 2023
Date: Wed. November 22, 2023
Event: FAU MoD Lecture Series (Special double session. November 2023)
Organized by: FAU MoD, the FAU Research Center for Mathematics of Data at Friedrich-Alexander-Universitat Erlangen-Nürnberg (Germany)
First session: 13:45H
FAU MoD Lecture: Prospects of formalized mathematics
Speaker: Prof. Dr. Michael Kohlhase
Affiliation: Friedrich-Alexander-Universitat Erlangen-Nürnberg. Carnegie Mellon University
Abstract. In (informal) mathematics (pure and applied) a human studies rigorously represented objects or mathematical models of the real world, comes up with conjectures about their properties, proves or refutes them, submits them for review and finally publication in the academic literature.
While it is commonly accepted that all of mathematics could be expressed and indeed developed in first-order logic based on (some axiomatic) set theory, this option is almost never executed in practice.
Formalized mathematics aims to enable computer support of “doing mathematics” by representing objects, conjectures, proofs, and even publications in formal systems, usually expressive logical languages with machine-checkable proof calculi, and highly efficient algorithms for automating various aspects of “doing mathematics”.
Highlights of formalized mathematics are
– machine-checked proofs of major theorems like the Kepler Conjecture,
– Feit/Thomson’s “odd order theorem”, or the four color theorem,
– search engines for mathematical formulae,
– synthesis and verification of computer algebra algorithms
– multiple libraries of formalized and verified mathematics
with more than 100.000 theorems/proofs each.
This talk will give an overview over the issues and results and introduces some of the techniques.
WHEN
Wed. November 22, 2023
13:45H to 16:15H (Berlin time)
WHERE
On-site / Online
[On-site] Room H16 Horsaal
GPS-Koord. Raum: 49.573365N, 11.028918E
Friedrich-Alexander-Universitat Erlangen-Nürnberg.
Cauerstrasse 7-9, 91058 Erlangen (Germany)
[Online] FAU Zoom link
Meeting ID: 624 1094 3213 | 694096
--
FROM 202.120.11.*