Robert Penner

I think it's becoming rather clear that ALL of mathematics will become possible to formalize rather soon. There are deep implications: 1. Mathematics becomes super interactive. Formalizations make it easy to browse, recombine, and build mathematical proofs from components. 2. Each new idea and paper can be checked much faster. The deep part is meaning and explanation. Validation is almost automatic. 3. Optimization and identification of new proofs can be done partially via agents, and humans can contribute much faster with great new ideas. Proofs from the Book are possible at scale. 4. Scientists and people at large can finally use mathematical artifacts as black boxes with trust and confidence. We can commoditize mathematical theorems. I think the mathematical enterprise also becomes very gamified. We can clearly see each unproven statement as a concrete goal, identify existing tools and directions, and focus quickly on what's missing. And everyone can contribute, with agents or through understanding. Soon, new languages and new theories will also develop, but the structure will keep growing steadily, with no mistakes and on fundamentally solid foundations. Hilbert's dream is becoming a reality. One important caveat: mathematics is by no means trivial now! It's just becoming extremely well-structured and laser-focused. I think the jump in capacity, quality, and scale will be massive. I also hope that our understanding of the big picture will remain solid, because there will be a lot to grasp.