The discipline Mathematics is at the core of engineering and sciences. Here we argue that AI methods are increasingly capable of processing existing natural language mathematics via automating formalization. This represents a promising direction towards creating systems that can expand the horizon of our mathematical knowledge and the safety of AI systems. Here I will highlight a few recent results that support this claim and conclude with some of the open challenges that lie ahead.

Bio: Christian Szegedy is a mathematician and a machine learning researcher who is known for discovering adversarial examples, architecting the Inception architecture for computer vision a co-inventing batch normalization. His current interest is AI for mathematics and Autoformalization.