Riding upon the fields on the horse of mathematics

This quote from Einstein resonates with me in a pretty surprising context. Einstein said this in a letter to Levi-Civita, praising what’s now called the Einstein notation. After watching Kevin Buzzard’s talk on mathematics being done with computers, I can’t help but feel the same way.

We’re doing mathematics on foot: on paper, in our minds. And there’s a reason. Interacting with computers is slow, and they often misinterpret what we mean. But that’s changing. Modern math libraries are using modern ideas from programming languages and they’re improving. Is there a threshold? A threshold for when they become widely used? Maybe it’s going to appear with undergrads using it to cheat on math tests. Maybe not. But it seems like it’s going to happen. A point of no return where it’s easier and more convenient to do research mathematics on a computer.

Note that this is how we’re doing it already. We’re already doing mathematics on a computer. You are using google and stack overflow in your research. You are using computers, but there’s no systematic way to check whether you’re right. And there’s no systematic way to add to the base of math knowledge.

Math libraries in languages such as Lean or Agda are slowly changing that. I have personally benefited from type-checking my thoughts in Agda, and others have too. Right now, it’s not easy to use these libraries, but as I said, that’s changing.

This is nothing more than my ponderings on the future kind of mathematics that might arise: a scalable, mechanistic, composable, and most importantly intuitive way of doing math. How will it look? It’s hard to say. But compared to where we are now – walking on foot – it’s probably like riding a horse. Or something faster than we can imagine.