In his essay on automation and mathematical research, Akshay Venkatesh ponders the effects of the hypothetical AI Aleph(0) on the mathematical community. In particular, the Aleph(0) will strongly impact the social fabric of our community.

In my talk, I will argue that formalization of mathematics is delivering benefits right now. Many of these benefits arise from the fact that formalization of mathematics greatly benefits from abstraction.

I will motivate my claim with empirical evidence. The community around the Lean theorem prover has developed a library of formalized mathematics that consists of roughly 1 million lines of Lean code. On top of this library, we have built the Liquid Tensor Experiment: a formal verification of the main theorem of liquid vector spaces, following up on a challenge by Peter Scholze.