+- MKLab (https://mklab.gr)
+-- Forum: [INDEX] (https://mklab.gr/forumdisplay.php?fid=1)
+--- Forum: MATHEMATICS (https://mklab.gr/forumdisplay.php?fid=3)
+---- Forum: ARTICLES (https://mklab.gr/forumdisplay.php?fid=13)
+----- Forum: AI AND TECHNOLOGY (https://mklab.gr/forumdisplay.php?fid=158)
+----- Thread: Embracing AI and Formalization (/showthread.php?tid=1558)
Embracing AI and Formalization - mklabgr - 08-11-2026
Embracing AI and Formalization
Articles
Jarod Alper’s “Embracing AI and Formalization: Experimenting with Tomorrow’s Mathematical Tools” argues that AI and formal proof systems such as Lean are likely to transform mathematical research, and mathematicians should actively participate in shaping this transformation rather than simply reacting to it. The article surveys five interconnected areas—mathematics underlying AI, mathematical formalization, AI-assisted autoformalization, machine learning for mathematical research, and the changing meaning of mathematics in the AI era—and describes Alper’s experience creating the eXperimental Lean Lab (XLL) at the University of Washington, where students learn Lean by formalizing undergraduate mathematics.
He emphasizes that AI can already solve sophisticated mathematical problems, discover patterns and counterexamples, and potentially automate parts of theorem proving, while Lean can provide rigorous verification that helps address the hallucinations and unreliability of language models. Although learning these technologies is currently difficult and frustrating, Alper argues that mathematicians should experiment with them now, develop communities and educational programs, and ensure that the mathematical community—not only computer scientists, corporations, or administrators—helps determine how AI will reshape mathematical research and education.
ARTICLE / ARCHIVE