Computers have transformed a broad range of human activities, from sales to basic research. Now, for an enthusiastic contingent of mathematicians and computer scientists, they are poised to deliver on a long-standing promise to do the same for mathematics.
The renewed excitement grows from discoveries that expand the scope of computer-assisted proofs of theorems, but also provide a new and more intuitive way of grounding new results to the bedrock foundations of mathematics, even as those results grow more complex. Tools based on these developments could help establish a growing library of certified results backed by computer verification. Along the way, it could change the culture of mathematics by making it easier for individuals to dependably add to this growing edifice.