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 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.

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 don't know, it sounds analogous to how the early Amish would have started their doctrine: "if the craftsman cannot do the task by hand, then they shall not use a machine ..."

I was thinking about that too.

I am probably being too optimistic, but wouldn't it solve the problem if peer-review had a pre-screening phase where you give a presentation about your work? Similarly to how a PhD presentation is given. It could give back the publishing power to the expert, rather than the journals.

Once you have validated that the knowledge you want to publish is yours and that you actually understand and own the work, then it doesn't matter if the paper is written by a LLM or if the LLM assisted you in doing the work.

This is a statement about what Tao values in the proofs that he consumes, as a world-class, human mathematician.

For many of the rest of us, mere consumers of mathematical results, it’s sufficient to know that a^2 + b^2 = c^2 was proven by somebody or some machine at some point.

The problem is that there will be far more formally verified proofs than that human mathematicians around the world can read, much less explain. What then? Would the role of mathematicians just become explainers of AI generated proofs?

I don't think the mathematicians are going to be able to make that work, because journals are already struggling to keep up with their review load, and AI seems like it will make that harder. So a solution that involves "journals will do a lot more effort to review each paper" doesn't seem practical.

It would work better as a bar for hiring, rather than as a bar for publishing.

What if the result is a counter-example? A fact that disproves the conjecture? Is that not publication-worthy?

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.

Tao has yet to produce work that outshines those whose work he studied and memorized. Not worth the reverence merely being a VHS copy of history.

He's a typical person otherwise, politically aware of how he barters for food; until proven otherwise this can be seen as little more than social moat defense.

To paraphrase a quote attributed to Upton Sinclair; hard to get a worker to understand something when their paycheck relies on them not understanding it.

The only interesting thing here is the frogs high up admitting they feel the heat.

I just don't see that to be true. If tommorow someone pulls a proof that n = np out of their ass but is not able to explain it, it will still have immense value.

This artificially limits mathematics to the limit of human ability.

It should be ignored and refused.

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

I saw an analogous argument posted on LinkedIn the other day from one of the opencode guys: the job of a programmer is still to be able to answer questions - from memory - about how the system works and why.

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.

[dead]