I believe this rule of thumb will come to fail. The combination of superhuman mathematical reasoning and synthesis in upcoming AI models plus the rapid build-out of scalable formal verification infrastructure means this exponential in math is going to take off quite explosively, and we've barely seen anything yet. Mathematics is going to decisively move beyond human ability fairly soon (within our lifetimes, if not much more abruptly). It seems abundantly clear to me that much of the work will only be immediately accessible to AI, and rather than trying to explain all of it back to humans we will rather focus on explaining the portions that humans would benefit disproportionately from understanding.

The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really hard to explain to humans, even by GMs. They can sort of explain that something is a good line but not why. Engines crush GMs and are considered ground truth even if noone really understands what is happening. Would it be a nightmare if math was the same, not sure. Especially for counterexamples LLM solutions seem fine. They stop humans from wasting time on pointless things. For proofs it gets more hairy but I think if it is formally verified a proof is a proof. Attribution is a problem (should the person who wrangled the answer out of an LLM get the credit, I guess so).

I think these are non-trivial epistemology and science theory problems.

I wonder what his views on the 4 color problem are. One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases. It doesn’t take an expert to state this.

Properly explain is an enormous grey area. Soon, I think, there will be proofs of results that are verified in Lean that are so long that no one will be able to “properly explain”. I don’t think they should be discarded.

Resolution of singularities is a famous theorem of Hironaka. Abhyankar claimed that no one truly understood the proof of the theorem. He said that he and Zariski couldn’t get through the paper with a full understanding. But everyone accepts this theorem as being correct.

I think any idea that is contingent on a human being in the loop, solely to the property of being a human is most practically doomed to fail, but is inherently anti scientific.

Science,at its core, does not care about the credentials or institutions. It cares about the results and to what extend they can be falsified.

This feel a bit like "we know all about physics, we can only get more precise" - moment

The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen. People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up.

We'll end up with incomprehensible math because comprehensibility isn't rewarded. No one is going to get a Fields Medal, or tenure, for digesting someone else's results.

Ive wondered whether a possible outcome of LLM slop is a retvrn to oral wisdom traditions. Ironically that's the most anthropological form of understanding and pedagogy.

But how would „what we value“ still be relevant?

Similar to Ai writing. Lots of bloat.

Absolutely. I feel I gain at least 10 IQ points when reading something on paper.

This is also the strategy I use for editing drafts of my books. I bring a printed draft to someplace nice (e.g. coffee shop or park) and read it all carefully, then I transfer the edits back to the .tex sources. I do several passes of this, until I feel the text + explanations are solid.

Reading on screen just isn't the same...

When I was in academia and had easy access to a good printer, I always did. I miss it now that it's easier to just read on my screen.

I think it’s more that he seeks to preserve and promote human understanding of mathematics, and sees that grappling with this new technology is necessary. One reason is that for human mathematical practices and institutions to retain legitimacy, they need to justify their value. As Tao explains, one obvious answer to that is made less obvious now with AI.

I think it's impossible to be half in. AI will eventually be better at things than people, and people will simply be rocks in the gears of progress.

The only thing to do is to be all in, or get run over.

If you are free from physical and mental labor, you are in fact, not supplying labor, and are therefore surplus to requirements.

> I don't know why anyone should care about understanding the results if the AI is better at math than us

This is a big if, right? AI can still generate subtle or even silly mistakes that any normal human, let alone a mathematician, wouldn't make. Besides, math is more than just getting a conclusion but to understand and to generalize new ways of solving problems. After all, mathematicians are a curious bunch. To quote Hilbert's epitaph: We must know. We shall know.

I’m not anti AI but thinking the human brain is obsolete and using it will become a hobby is a dystopian view of the future where no one has any agency anymore. By your logic since our brains provide no value why not just shoot ourselves in the head while we’re at?

What if the better routing leads to an outage that the AI can't explain or fix and all the humans who might have understood it were laid off or otherwise unavailable?

In some sense "understanding" (understanding if it is true, if it is important, how to use it) is about the only bottleneck in math. Any theorem that you can write down or imagine is already true, false, not provable already. In some ways we can already start iterating through all the theorems. We will never get to the end (or really get very far down the line) and most all of them be trivial (I think the Busy Beaver[1] project is a fascinating example, ymmv).

I am wary of AI in all aspects I am seeing it in but in many ways in mathematics seems to me the least troubling. It will change things in and the field will not be the same. Blacksmithing has not really gone away. You can still work as a farrier, if you like that sort of things. The tools that replaced a man working over a forge with a big hammer are part of a giant industry that is still producing works for the modern world.

[1]: https://bbchallenge.org/8226493

How is either of those situations more or less like a hobby than the other?

Somehow, I feel that progress, in your understanding of what progress is, loses all meaning.

It will be the same as before: some effort will go into checking proofs and the other into creating them. AI speeds up both.

You should give it a try. Tao is a wonderful person and is trying to help humanity.

Out-of-hand dismissal of Terence Tao is certainly a take.

And the term "artificial intelligence (AI)" has been the name of the field for 70 years and counting. If anything, "LLM" is a misnomer that's been lingering around since 2018-19. When the term was coined, these systems were relatively small, experimental, and could only produce impractical facsimiles of the English language. This is obviously no longer the case today.