Elektrine lite

← Feed

@rook@awful.systems

2026-09-03 17:01 UTC

Terence Tao observes that an llm may solve a complex mathematical problem without usefully improving the state of mathematics, because the intermediate results of the process themselves can have significant value. mathstodon.xyz/@tao/117207849921390904 But such an incomprehensible proof would not be the primary value of the exercise. The process of starting with one ansatz, discovering the precise obstruction preventing it from working, adjusting the ansatz to (partially) eliminate that obstruction, and then iterating, would almost certainly reveal important new insights about fluid mechanics that would not have been feasible to obtain by other means. Crucially, this iteration would only work well at producing such insights if the iterator did not have access to the final ansatz in advance, as this naturally inhibits the exploration of alternate routes to the ansatz that are superficially “dead ends”, but in fact end up being highly instructive in the nature of their failure. But there is now a scenario in which an autonomous AI harness, backed by an enormous amount of computational resources, performs this entire iteration internally, and ends up producing the final ansatz, and thence the solution to the Navier-Stokes regularity problem, while the AI company running the harness keeps the process to arrive at that ansatz almost completely out of public view. Technically, one of the most prominent open problems in mathematics would now be solved; but there would be almost no value added to mathematics as a consequence. It is theoretically possible that with some herculean (and heavily AI-assisted) additional effort by a third party, some portion of the process could be reverse-engineered to recover some actual insight and understanding from the solution; but this would be a far less efficient process than if the solution had been obtained via a diverse combination of both human mathematicians and machine assistance as mentioned above. mathstodon.xyz/@tao/117207855800042681 He’s not the first to have pointed this out, but I think this was a better summary than similar posts that I’ve come across and at least partially understood.

Replies (2)

  • @sc_griffith@awful.systems 2026-09-03 17:47

    terry tao grimly putting the hotdog suit on

    Open ##4613730

  • @blakestacey@awful.systems 2026-09-03 19:59

    We don’t need more of mathematics to look like the Four Color Theorem (“proved”, but with no insight gained), with the added problems that the “proofs” are now far more laborious to check even for technical correctness, theorem-proving software is less reliable, and oh yeah, we’re holding the population of Memphis to the exhaust pipe of a diesel bus to make it work.

    Open ##4614310