In 1976, K. Appel and W. Haken announced a computer-assisted proof of the Four Color theorem, solving a long standing open question in graph theory. Since, experimental mathematics have gained momentum and computers have even changed the very nature of peer-reviewed mathematical proofs. This phenomenon can be observed in a broad spectrum of fields, including number theory, dynamical systems, combinatorics, etc.
A vast variety of software is available today for doing computer-aided mathematics. Tools, and the algorithms they implement, are usually grouped in two partially overlapping categories: the symbolic ones, typically computer algebra systems, and the numerical ones. This talk is about a different flavor of software for doing mathematics with a computer: proof assistants. So far proof assistants have been mostly used for research projects in computer science, often related to program verification. But proof assistants, and in particular those based on dependent type theory, are receiving these days an increased attention from users with a background in mathematics. Designing formal libraries about contemporary mathematics raises specific issues and challenges for proof assistants, that we will discuss.