Post #4070525

2026-07-24 19:17 UTC

Am I right in understanding that almost all the big name results in LLM-derived math recently come from big publicity projects in which someone spent ungodly amounts of money to have the thing nondeterministically fuzz huge numbers of independent random sees of outputs around a topic, putting out simulacra of ideas which could be then deterministically algorithmically checked? In fields where something like finding one counterexample to a conjecture would be a big deal, or where you just need to try a huge number of possible solutions until you happen to hit on one that works, rather than follow a long train of logic?

Replies (1)

@lagrangeinterpolator@awful.systems 2026-07-24 19:54

Among the three big results I’ve looked at (unit distance problem, cycle double cover, Jacobian), two were counterexamples and one of them had a short 3 page proof using ideas from the 1970s. The Jacobian conjecture is an extreme case because a single counterexample is enough (for unit distance, you technically need a family of counterexamples), and it is easy to check with very basic computations. It is telling that all of these announcements came from OpenAI or Anthropic employees, who presumably have unlimited resources. Nobody really knows how many resources they spent on this, or what else they tried. Nobody really seems to care about this question, either. What I’m more worried about is many people starting to use AI to try and prove small lemmas for them in their projects. Of course, a $200/mo subscription is absolutely necessary to them. This honestly feels like a repeat of Claude Code back in February. The software engineers eventually realized that AI is absurdly expensive after the companies realized that spending $14000/mo to service a $200/mo subscription is a bad idea. If the AI vendors couldn’t squeeze money out of rich software companies, what exactly are they gonna get out of poor mathematicians and universities? Also, there is the cognitive decline caused by overuse of LLMs that has yet to set in.

Open ##4071247