Symbolic Computation Group

In the past 50 years immense progress has been made in the domain of formal computer-understandable mathematics. Today about a dozen systems exist that represent person-century amounts of investment and that have been used to obtain flagship formalization results like the proof of the Kepler conjecture. But despite its potential to be a transformative force on mathematics, even our best formalizations are merely case studies in comparison to mathematics as a whole.

In this presentation I describe the current state of formalized mathematics from a big picture perspective. I identify long-term challenges and present potential solutions.