Formal Mathematics for the Masses

The campaign to transform traditional mathematical practice into a formal discipline appears to have been a great success. Several sophisticated proof assistants have been developed, a great deal of mathematical knowledge has been formalized, a growing number of researchers in computing and mathematics are now using proof assistants to check the theorems they prove, and a new area of computing called formal methods has been established in which …