The Formalized Mathematics Revolution in the Era of Large Language Models

The event "The Formalized Mathematics Revolution in the Era of Large Language Models" was hosted by UKTI.HUB at UCL on February 14, 2025, featuring keynote speaker Huajian Xin, core developer of DeepSeek AI-Prover-V1.5. His lecture attracted nearly 200 on-site attendees and over 10,000 online viewers. A panel discussion followed, with Liang Ge from UCL, and other scholars from Peking University and Imperial College London exploring AI’s impact on formalized mathematics. The event concluded with an interactive Q&A session and networking opportunities, where attendees engaged in further discussions with Dr. Xin and panelists.

🎉Many thanks to UCL Chinese Students and Scholars Association and all supporting partners for their contributions.

🌟Dr. Xin’s presentation covered the evolution, challenges, and applications of formalized mathematics, which involves encoding mathematical concepts in a machine-readable format for rigorous verification. While computational tools have advanced the field, challenges remain, such as large-scale proof formalization and integration hurdles with…