Abstract: Formalizing mathematics into machine-checkable logic is essential for advancing scientific rigor and enabling powerful AI reasoning. However, the process of translating informal mathematical text into formal languages remains a major bottleneck. This talk explores the challenge of autoformalization—the automated conversion of natural mathematical language into formal logic—through the lens of Euclidean geometry, one of the oldest and most foundational domains in mathematics. I will present insights from our recent work on LeanEuclid and PyEuclid, which demonstrate how modern Large Language Models (LLMs), combined with formal methods, can help bridge the gap between informal and formal mathematical reasoning.
Bio: Xujie Si is an Assistant Professor in the Department of Computer Science at the University of Toronto. He is also a faculty affiliate at Vector Institute and an external affiliate member at Mila, the Quebec AI Institute, where he holds a Canada CIFAR AI Chair.