Thursday, December 1, 2022, 16:00
online
(for the zoom link contact michael.spira@psi.ch, marco.rocco@psi.ch
or max.zoller@psi.ch)
Michael Douglas, Stony Brook University
Abstract:
We make the case that over the coming decade, computer assisted
reasoning will become far more widely used in the mathematical sciences.
This includes interactive and automatic theorem verification, symbolic
algebra, and emerging technologies such as formal knowledge
repositories, semantic search and intelligent textbooks.
After a short review of the state of the art, we survey directions where
we expect progress, such as mathematical search and formal abstracts,
developments in computational mathematics, integration of computation
into textbooks, and organizing and verifying large calculations and
proofs. For each we try to identify the barriers and potential
solutions.