An inscrutable 1000-page Lean proof may have low transmissibility amongst humans, yet extremely high transmissibility amongst AI mathematicians.

Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.

Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.

What is the difference between "beauty" and "elegance" of a proof?

You are mixing a lot of categories here -- beauty, verbosity, utility, elegance, insights.

Why all that when you just need one thing: truth.

Most mathematicians don't take pride in their results having no applications. That's just not true. Maybe some quirky pure logicians or something. But otherwise 90%+* of mathematicians I know would be at least satisfied if not thrilled for their work to be used by others.

*Completely made up statistic.

Are you sure that’s «most» mathematicians?

At the universities I’ve been to (as a student and now faculty), «applied mathematics» and «statistics» have been the two largest divisions. But perhaps that’s a bias from engineering-heavy universities?

You put it perfectly. And all these AI math startups don't actually care about mathematics. They are just using it as a proxy for general reasoning, with the VC pitch being some kind of world domination after they crack these problems.

I think you may be interested in more abstract things. In this case, let's say you're creating a program for a 3D printed thing, and you have to fit a diagonal cardboard in a rectangular box, you'd like to be sure that the Pythagorean theorem holds even in cases where you haven't tried it out.

> For any practical application, you are only interested in finite set of concrete identities

I do a lot of numerical work in settings where computational efficiency is useful.

In my work, most cases you can do numerically using integration or Monte Carlo sampling or whatever.

It’s slow. It often pays to find a closed-form solution. Even if it’s just a starting point that needs refinement.

To put in terms of the Pythagorean theorem: Proving the Pythagorean theorem gives you a relationship that’s reliable, fast to evaluate, and general. Proving individual tuples gives you none of this.

That doesn’t even touch on how theorems give us a glimpse at deeper structure and truths. Proving a bunch of right-triangle tuples will probably never lead you to the rest of the identities in trig.

The current commentators are surely missing the fact that this comment is sarcastic.

You meant this as satire, right?

How is this relevant here? AI helps you understand the why -- it literally discovers the proof and hands it to you with explanations. It hands you the proof that you would have otherwise not found easily.