In the first year of university mathematics we are taught about the axiomatic structure of mathematics, how we build a solid structure of correct statements and their proofs, that can lead us to the stars (modulo Godel). We are taught that every correct statement can (and should) be justified back to the axioms.

Working research mathematicians build their work on libraries of published material and hope that everything quoted is justifiable back to the axioms, so that their new contribution is also. This is also how new work is judged so if the system works perfectly then this satisfies the axiomatic dream, even though most researchers have little interest in going back to the axioms themselves, indeed much of the work that would be necessary to do so would be irrelevant.

However we are all familiar with proofs that are a little shaky, perhaps missing a few details for us to be 100% sure, or even with a hole that "seems fillable". Professional mathematicians work with a notion of "robustness of proof", that even if a few details are awry one can be confident of the big structure. Thus even statements with a (formally) incorrect proof form part of the accepted literature, which seems like an odd way to proceed.

How should the successes of proof verification software affect the community's view of what constitutes a correct proof? How will it? In this talk we bring together several threads to investigate these questions, and propose some objectives for the future.