← Back to context

Comment by timmg

3 hours ago

As a non-mathematician, I've been wondering if LLMs will be able to leverage their knowledge across all domains to help build a "simplified/unified" version of math.

Like, I think there have been attempts at this across the field. (I could be wrong!) But it requires a lot of labor and a lot of cross domain knowledge to complete. Both things that AI have.

As a mathematician, I am looking forward to the day when nearly all of undergraduate mathematics and many of the lower level grad school math books are encoded in Lean (a proof checking language). Often I find that theorems are not stated precisely enough and I have trouble finding the exact statement of a theorem without digging through math books in my library. It would be nice if we put the physics and chemistry books into Lean also.

Simplifying all of math is another endeavor, but I imagine that you could have a bunch of LLMs trying to shorten existing Lean proofs.

  • I was pretty upset when my algebra professor tried to make us learn proof about n-dimensions matrices and what not. It was an undergraduate engineering degree and the vast majority of the formulas would mostly have up to 3 or 4 dimensions. That derailed the whole year (it's not like maths was the only subject). Complete proofs and theorems have their places, but learning stuff do need levels. The spherical model of the earth is good enough in 2nd grade (when we were first learning about geography (continents, seas, mountains, plains,...)), no need to do a full treatise there.

Math simplified? The "basic" math (say less than graduate math) is already simplified and minimized and refined. Yet most people have trouble understanding and mastering it.