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 tutoring. After a short review of the state of the art, we survey directions where we expect progress, such as organizing and verifying large calculations and proofs, making computational mathematics easy to do, and integrating formal documents from many sources into a coherent whole. For each we try to identify the barriers and potential solutions.
Thackeray Hall 704