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.
there have been explicit attempts at this in the past. Nicholas Bourbaki was the pseudonym of a group of French mathematicians who had this goal mid 20th century. You can see e.g.
It has many benefits, and many people appreciate the books. It also has many downsides. For example, they started publishing in 1939. As part of this, they needed to work through the basis that most other mathematical objects are defined in terms of (they used sets).
Unfortunately for them, contemporaneously with their work, other mathematicians were beginning to define mathematical objects (categories) that can be an alternative basis for mathematics, which many modern expositions prefer to sets. So, their approach either
1. needed a massive "refactoring", or
2. would be hopelessly dated.
They ended up going with the approach that is now dated.
It may sound peculiar that mathematics can be "dated". But it very much can. The mathematics community can go through many different styles for how to explain/collect mathematical understanding. Different styles can have different benefits, and be easier/harder for different subfields. A simplified/unified perspective will necessarily privilege certain perspectives.
It is analogous to how you might want there to be a simplified/unified (set of) libraries for programming. Perhaps that everyone uses. This sounds nice, and many programming languages do this with their standard libraries. But these always make concessions! I'll speak about Rust's, as I'm most familiar
1. fallible allocation or infallible allocation?
2. C-style strings or (ptr, len) strings?
3. Should interfaces take as input &mut [T] references, or should they take as input T in an "owned" way (this would make compatibility with io_uring easier)
for each, it is not that one answer is right. Both can be argued for. You have to choose one. The one choice may not be satisfactory for every practitioner though.
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.
I'd say people have trouble understanding basic math because it's extremely simplified and minimized.
When you don't know a topic, the way to understand it is to see lots of examples from different angles related to things you know. The simplified formulas are good after you get that initial intuition and have to put them to work, but usually they're terrible at conveying how they should be used or why you should care at all. The history of how new fields of math are usually a much better approach to teaching it than a raw theorem-proof-corollary teaching style.
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.