GoKawiil$\begingroup$
Medieval mathematics was a highly personal craft, with knowledge of mathematics and methods being treated as a liability (for better and for worse) and having that knowledge was treated as secret knowledge that your livelihood depended on.
The reputation of a mathematician depended on knowing techniques others did not know. Mathematicians frequently challenged other mathematicians to semi-public mathematical contests. The two gave each other a set of problems. Whoever solved the problems the fastest, or the most problems in a given time, won the contest and could secure their funding and social status, while the unsuccessful contestant faced public embarrassment.
This created a strong incentive to keep discoveries secret. For example, Scipione del Ferro is now known for discovering a method for solving depressed cubic equations in ~1510. But he kept this method hidden for 20 years because this knowledge gave him professional security. He disclosed the method to his student only on his deathbed.
So knowing a particular formula, algorithm or technique could give the individual significant societal powers and connections; in a way that simply is not possible today. This attitude and orientation of mathematics continued well into late Medieval Era and later; Leibniz complained to the Royal Society after accusations of taking Newton's framework and simply just changing the notation. The Royal Society appointed a committee to investigate (while at the same time Newton was president of the Royal Society), which concluded Newton was the sole author of calculus. Much of the dispute stemmed from Newton’s decision to delay publication and keep his framework a secret.
Today, results are encouraged to be published rather than delayed or kept in secrecy (albeit there are major issues with how journals operate and paywalled papers). Incentives are rather to write papers and the funding problem has largely transitioned to a system of writing grant applications.
This largely social contract appears to be changing, with the advent of large AI companies going after famous problems for PR. Theorems have become cheap. A lot more people, with enough technical skills, can generate largely correct proofs for many problems. Especially undergraduate mathematics, but also graduate problems and previously unsolved problems. These proofs that LLMs can spit out can even be prompted to give a full Lean formalization of the proofs. Some have even gone so far to call the current situation “the fall of the proof economy”.
Now, there is an entirely separate issue (that I will not touch on here) on what to do with these AI slop Lean formalizations that no human has a hope of understanding. But ignoring the issues with slop proofs and the doubt cast on Lean's own soundness, it seems that anyone with enough money to spend on compute can unleash a swarm of typewriter monkeys in advent of rumors of some known problem being close to a possible solution.
For the recent claimed counterexample of Navier–Stokes, Capital&Compute estimated a cost of ~\$6.5 million on compute. TensorFeed estimated a cost of ~\$10–\$15 million, factoring in other costs than pure tokens, and Business Insider estimated a total cost of \$10–\$40 million.
Regardless of the true cost, it seems that professional mathematicians now need to wary about what they put into a LLM and think hard about how to disclose and publish a result. The ability to spend millions of dollars on compute to just grab the full formal proof before anyone else can react is only something companies with large amounts of capital can do. The technology is also being gatekept; because of the insane costs it takes to set up the infrastructure, it is not feasible for any single individual to do it.
... continue reading