If you can't understand what the machine has done, math is not being done. Math is not pushing symbols around to find sequences that follow all the rules. Math is the process of understanding how those sequences of symbols map to meanings. If you can't follow the proof but have validated it's correct, all you know is that it's a proof of something. Is it a proof of what's claimed in the adjacent plaintext? Who knows!

Math is about clear communication between people first and foremost. That's why Shinichi Mochizuki's claimed proof of the ABC conjecture isn't accepted - he's unable to communicate it to enough mathematicians to get a consensus on its validity. LLMs generating Lean proofs are basically following that same schema. Sure, something has been proven. But what? Where's the clear communication explaining it to the satisfaction of other mathematicians?

The mistakes that lurked in radium, in arsenic, in leaded gas, in fallout downwind of nuclear tests ... all had the best tools that the previous generation knew.

None of them were okay. Those were small small tools with few (sometimes only one) uses.

Generations earlier, famines, diseases and lead-leeching plumbing made rulers insane and entire cities of people die without any help from the "best tools".

Scifi is always written about the best tools. The issues arrive in the tools and in the hands that wield them both.

There are a few increasingly powerful companies that own the frontier models that can produces these results. In the future, it may only be these models that understand the results. Should we be beholden to a few companies for basic understanding of foundational principals?

The "top layer" of maths being this is one thing. Now imagine another layer of this. Then another. Then another. Then another.

At one point intuition helps to build out usage of the math itself. See stuff like "oh I can do rotations through matrix multiplication"-style ideas.

It is helpful for us to be able to reach for those tools quickly. The more tools that require advanced prep to use, the less we'll be able to use the results in easier contexts. Everything will be hard

Of course nothing really prevents people from looking for the simpler tools and proofs. Lots of math stuff starts off complicated and gets simpler.

Just important that this is still a goal in mind

Yup, and it always has been, we don’t even understand how our bodies or minds work, yet we use them everyday

The amount of unimaginable complexity contained in a seemingly very tiny amount of matter to us, is incredible, and it’s all around us in nature

We’ve never had the capacity to fully comprehend neither ourselves nor the environment we live in. But we do our best, and we do survive and sometimes even thrive

> Why not? If mathematicians in the field cannot understand the papers, but tools at our disposal can (...)

How can you tell?

Sounds like a disassembler.

Because the tools don't understand the papers either. We know for a fact that:

1. These tools are wrong a significant % of the time

2. They have an upper complexity bound where they start to fall apart

Relying on AI to check AI papers is a terrible idea

because the tools can't? Lol. That's not how it works. Am I in the twilight zone?

All this anthropomorphism of literal statistical text generators.

Yes they exhibit generated sentences of text that describe coherent responses about a topic when there's an inordinate amount of research material in the training data from which they are distilling sentences of sound and rational thought. That's the ONLY way it can possibly work. There are so many scenarios where the training data isn't setup like that and low and behold the generated responses are just literal garbage.