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.
Simplifying all of math is another endeavor, but I imagine that you could have a bunch of LLMs trying to shorten existing Lean proofs.
https://en.wikipedia.org/wiki/%C3%89l%C3%A9ments_de_math%C3%...
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.
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.