Recent advances in automated reasoning and interactive theorem proving have made it possible to formalize and mechanically check substantial mathematical theorems, such as the prime number theorem, the four color theorem, and the Jordan curve theorem. In particular, a number of interactive proof assistants have been developed to help users manage libraries of definitions and theorems, and fill in the inferential details of a mathematical argument. Automated methods are also often used to verify calculations that are too long and complex to check by hand. As mathematical proofs become more complicated and, increasingly, rely on extensive calculation, this gives rise to an exciting interaction between traditional methods and computational means of verifying mathematical claims.

The present issue is devoted to recent advances and new perspectives in this field, including descriptions of formalizations, thoughtful reflection on the future of the discipline, novel insights, innovative research directions, and critical assessments of the current state of the art.

Extended versions of work previously published in conference proceedings are eligible for submission but authors should make it clear how their submission improves upon the conference publication; in those cases where Cambridge University Press is not the publisher of the original conference proceedings, authors should take care to avoid infringing that publisher's copyright. Authors who wish to discuss potential submissions are encouraged to contact the guest editors.

Papers should not be longer than 35 pages; shorter papers are obviously welcome.