Please note: This seminar will take place in DC 1304 and virtually over Zoom.
Florian Rabe
Friedrich-Alexander-Universität Erlangen-Nürnberg
In the past 50 years immense progress has been made in the domain of formal computer-understandable mathematics. Today about a dozen systems exist that represent person-century amounts of investment and that have been used to obtain flagship formalization results like the proof of the Kepler conjecture. But despite its potential to be a transformative force on mathematics, even our best formalizations are merely case studies in comparison to mathematics as a whole.
In this presentation I describe the current state of formalized mathematics from a big picture perspective. I identify long-term challenges and present potential solutions.
To join this seminar in person, please come to DC 1304. You can also attend virtually using Zoom at https://fau.zoom.us/j/4879450888.
200 University Avenue West
Waterloo, ON N2L 3G1
Canada
