If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?

I don’t think it’s pointless to spend time trying to prove a conjecture which is ultimately false if along the way you figure out a bunch of different true variations on the conjecture, which is how mathematics actually works. This is something I’m a bit worried about with LLMs since it gets you to the end too fast.

I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?

Maybe that will be true when it's math with practical applications, but most theoretical math isn't like that. If it's not practical and it's not for mathematians to understand, what good is it?

People say similar things about automation of software engineering. Different, but similar.

I'm deeply suspicious. I do not yet have a concise statement for why, but a lot of literature on the sociology of knowledge work sort of points at my thoughts.

Section 5 of the Thurston article cited by Tao touches the elephant. Raduchel's article on the economics of software [2] also touches it.

I've tried to put words to this for a few years. I think I'm just going to start writing versions of it as see if that helps me shape the thought into something more concise.

So, in the spirit of this article's style, here are some postulates:

1. There is a sociological process happening in the production function during knowledge work.

2. That production function and the associated sociological process spans years or even decades, and must outlast many of the artifacts that are produced during the early years of the function.

3. You cannot get the right lines of code or the right theorems proved without running that sociological process alongside the artifact production process.

4. It is impossible to completely separate the sociological process from the artifact construction process. If you just iterate on artifacts then too much of the required hidden state is lost to make progress in the right direction. This is true even if you include distilled artifacts capturing pieces of the sociological process (eg meeting notes, documentation, commit logs, prompts).

5. So you need that sociological process, or something like it, to still happen.

6. For a lot of knowledge work that process plays out in extremely high-fidelity social interactions [3] that we have not yet captured in the datasets that would be required to reproduce those dynamics.

7. And even if we do collect that data, our current architectures and training algorithms and hardware would be useless given the size of the datasets.

So: the technology today gives us the ability to iterate on the production of artifacts. But it does not sufficiently simulate the social process which gives rise to the Right artifacts.

This isn't exactly what I actually think, but it's a version of the thing that I intuit when I watch heavy use of AI in both software projects and formalization projects. And simulating that process feels way harder than people are currently assuming.

[1] https://arxiv.org/pdf/math/9404236 Section 5.

[2] https://www.nationalacademies.org/read/11587/chapter/11 pp 166-168.

[3] there is a reason we still gather in-person around white boards, and why doing so is more crucial for some types of work than others.

It will be interesting to see the evolution of journals in the next ten years for sure. Have they outlived their usefulness? Maybe everyone will just upload papers to arXiv, along with a copy of the formal proof.

For an exhaustive search, if you can explain to me: - how to exhaustively list the cases that need to be checked, and why that method is exhaustive - how to check each case, and why that works and then conclude with "we've had a computer do this exhaustive search, and the result came up as X", for me that satisfies completely understanding the proof.

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

Just burn lots of tokens on the frontier model of your choice to let the AI find a high-level argument why the four color theorem holds. :-)

--

Seriously: since there exist quite a lot of readers on HN who are both hardcore into AI and mathematical problems: This is a challenge for you.

I am looking forward to seeing an announcement of a novel high-level argument why the four color theorem holds on the first page of HN in at most a month. :-D

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

Hmm, doesn't it take an expert to explain why those cases are exhaustive, and why the code that checked them is correct?

Tangentially, I'm not a mathematician but I wonder if one "opaque" proof that is too complicated for anyone to understand, but that we know is correct via formal verification, might end up being built on with "transparent" human-understandable proofs. For example, it's my understanding that there are many conjectures that have been proven true conditional on the riemann hypothesis being true. In that case, an opaque proof of the riemann hypothesis would enable those conjectures to be known and built upon

Nowadays the proof of resolution of singularities in characteristic zero is considered something you can teach in an intro algebraic geometry course, though. The concepts have been absorbed and are now much better understood. 4CT is very different because so much of it is exhaustive case analysis; you can understand the high-level ideas of the proof as a bright undergraduate, but you still can’t check the cases by hand

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

The incentive will be to be able to publish in a top tier journal. I suspect what Tao is advocating for is having journals reject such manuscripts.

> No one is going to get a Fields Medal, or tenure, for digesting someone else's results.

I'm sure no one gets a Field's Medal if others can't digest their results.

> The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen.

He says it shouldn't be able to published if they can't explain it. Publishing it is the reward.