Over at Quanta magazine, Kevin Hartnett has an interesting article about using computers in the service of Mathematics. That’s nothing new, of course, but this isn’t about numerical methods or LaTeX, it’s about using computers to help develop mathematical proofs.
Even that notion isn’t new. There is, for instance, Coq, which has been doing the same sort of thing since 1989. What is new is that Mathematicians are trying to capture within another theorem prover, Lean, all known mathematics, or at least all of undergraduate mathematics. That’s a huge undertaking and they’re still only about half done. The hope is that with that knowledge, Lean will know enough to start help proving theorems.
According to the latest Mathlib Statistics, there are currently 19,305 definitions and 41,552 theorems in the system. You can, yourself, play with the system if you like. There are instructions for installing it on all of the usual operating systems or even for running it in a browser, although that will be much slower than a regular installation.
If, like many of us, you come from a Mathematical background, you’ll probably find the article interesting and may want to try the system out.