Folks really want to decide if this is pro or anti and respond to that. It's neither.
In a world with only LLMs doing the day-to-day of proving, you still want more than just proofs dumped out as soon as they pass adversarial review or formalization. The first proof code that passes checks may be a mess that's hard to build on; the path to a result, including failures, is full of interesting stuff; naming, generalizing, linking, and organizing things are tasks that move us from today's raw material to tomorrow's future directions.
Folks get this about code: "it works" isn't the same as "it's good." We knew it before LLMs, out of practical necessity as projects became hard to build on.
An odd thing to me is it would not be that big a concession for the labs to openly talk about the difference between the math artifacts they're releasing and what mathematicians do. It's analogous to the Claude's C Compiler post noting it wouldn't replace a prod C compiler. They could talk about paths from a rough initial product to 'production' math, say they hope future models will continue to improve as math collaborators and expositors, and so on.
For the compiler, the gaps would be trivially obvious to their customers, so it was an obvious call to acknowledg them. With their math output, the difference between a proof dump and the kind of well-written, contextualized mathematical program the community pursues is apparently subtle and deep enough the companies can't get themselves to acknowledge there is any difference. So the companies self congratulate and then are yelled at on the Internet instead.
(Ant seems to have wised up a tiny bit about this compared to OAI, and e.g. Ant handed a recent result to some experts in complexity theory to understand and refine and publish rather than just dumping a Claude-written PDF.)
And yes the drug discovery piece was weird. There are good relevant points: it'd be good to understand pharmaceuticals better (helps us find others, understand side effects, etc.); when we get a mystery result, it's worth effort to try to work our way to proper understanding; anything that could help us understand (reasoning etc.) shouldn't be hidden. But as presented it's both not a lot like math and accidentally a lot like those "would you choose..." questions that always get so much engagement on social media.
Yep, it's unfortunate how often folks sort something into pro or anti then reach into their bag of anti or pro arguments without relatively little attention to the specific thing they're talking about.
The Sendov example has a piece coders will hopefully recognize: he found a formalization that was 1/6 the amount of code of the original one. And the analogy with code goes further--the messy version will run/pass the proof checker, but the one that's been cleaned up and made sense of is a better foundation for future work. That's true even for future LLM-assisted work.
So it's not about whether mathematicians take advantage of LLM help (Tao favors that) but, more or less, whether the point of math is just to make a bigger version of the GitHub dump vs. everything else: readability/comprehensibility, negative results that fill in the map around a problem (not just 'lighthouse' theorems), organizing results to plan out future work, and so on.
Making things understandable is part of intelligence as much as producing the initial artifact is. Even if the proof checks out in Lean (or the code runs and passes QA) if it's a mess, it will be hard to use it to do anything further.
This does not only matter doing cutting-edge mathematics. This, about the 'digested' version versus the original, should feel familiar to some folks here:
> This formalization is more streamlined than the original formalization (it has about 15,000 lines of code, compared with around 90,000 for the original proof).
and if you've ever tried to turn an overly vibed piece of code into something that makes sense:
> it has taken me several days (with heavy AI assistance) to perform such a digestion, to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas
If you see something that is confusing or overly clever, please don't assume it must be for some good reason you don't understand and move on--ask questions, get it simplified, try to get it worked out. Future you will appreciate it.
About the argument that a beam's strength:weight ratio worsens as it grows: do the artificial structures humans use, like house frames or bridges' trusses, recover strength:weight ratio? Would a theoretical giant with a skeletal structure like a bridge or a house's frame be better off than one with a human-like skeleton of the same material? (And, related to another comment here, guessing the actual structure of bone produces some improvement relative to something solid?)
> do the artificial structures humans use, like house frames or bridges' trusses recover strength:weight ratio?
There is some improvement from computer design. We have better tools to know the margins that allow us to remove as much material as possible, things like that. So we can tweak existing designs to make them more efficient, like adjusting the section of beams to make them as strong but with a few percent less materials.
But the major improvements come from using different materials and new techniques, side-stepping the scaling issue.
For example, we could not scale old arch bridge designs very far. Getting steel beams let us build truss bridges, but even these cannot be that long in a single span. Suspended bridges were a step forward, with the improvement coming not from better beams, but from removing them altogether. Then, cable-stayed bridges solved some issues with older suspension designs and we can now have very large spans. Every time, scaling up is enabled by a change in strategy.
> Would a theoretical giant with a skeletal structure like a bridge or a house's frame be better off than one with a human-like skeleton of the same material?
Looking at things like elephants and dinosaurs, there certainly would be a way to have bones strong enough to support a 10m high human-like thing. Now, whether we would recognise that thing as human, I don’t know. Every time the problem was solved, there were significant compromises. I am not sure a giraffe’s vascular system could sustain a human’s brain. Elephants are not particularly agile. Whales cannot get out of the water.
Actual bone does incorporate some things we would consider "architectural" or "engineering" techniques to do more with less, not least of which they are composite materials and not mere rocks. They remodel the structure dynamically to respond to stresses as well.
Hard to make big predictions, but it sure looks like at least this level of capability is going to be available in the open and relatively cheap to run.
The 'floor' has gone up: today's model a bit behind SOTA is like model releases that were blowing people's minds a few months ago. Compared to, say, DS R1, this is far out stuff.
This, Luna, and (if it's good in practice) Laguna S are also fast and light not just cheap. And, as happened before, DeepSeek's first but other open model makers likely follow.
And a small, fast model taking small steps is...fun? More like working with code.
One read is 1) they're getting a lot of traffic for Flash, 2) they've said they're updating Pro soon and expect that to lead to a traffic spike for Pro, but 3) that would leave them overloaded, so 4) they're going to raise prices to avoid it.
It's interesting that most open models adding 1M context did it in a way that reduces KV cache size (though DeepSeek was the most aggressive, using compressed attention on all layers), but only a couple providers turned it into a discount on cache reads.
The field of mathematics is smart about this and knows the difference between a pile of Lean code and understanding, and mathematicians try to get from the unintuitive explanations to something that makes more sense, e.g. https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the... (where incidentally Tao used a chatbot to help take apart the problem, but with a lot of interaction and work from his side).
Making things understandable is mathematics, and more generally a kind of intelligence, and is crucial to continued progress. You couldn't use algebraic geometry to disprove a conjecture if people hadn't organized (what could have been just) a pile of random observations into something called algebraic geometry.
Historically LLMs have done best where it's possible to train using an objectively verifiable reward function. Computer programs are pretty good on this front and so are Lean proofs. (Of course, they don't only do things you can RLVR heavily, but those have progressed fastest.) Not sure where 'making mathematical knowledge more understandable' falls on that spectrum.
Understandability isn't only important for advanced math. Keeping computer programs from becoming a mess is a challenge in high-level organization too, and the chat with the user is an explanation task. If you look online at what people say about large LLM-built codebases (SlopCodeBench is a neat effort to make make it concrete, but common wisdom seems to mostly agree on the general problem) and chatbot prose, I don't think everyone considers those solved problems!
It's hard to tell how thoroughly the labs grasp and care about this at an organization-wide level. I'm sure at least some maybe-results exist inside labs but haven't been published because the humans couldn't verify them and didn't want to be embarrassed with a false result. (Maybe also why counterexamples are a lot of the first results published: often simple to verify, even if hard to obtain.) A good sign would be if results in a few months come out more like what mathematicians consider well-written papers explaining results in a more intuitive way, fewer shocking announcements of bare counterexamples in tweets. It's probably a slow climb to get there.
Singer-songwriter Silvana Estrada named an album released last year Vendrán Suaves Lluvias (meaning There Will Come Soft Rains). She talked about how she and her brother read The Martian Chronicles as kids and she remembered the Sara Teasdale poem quoted at the end. She said she composed the songs at a difficult time in her life and, I guess, something about that image in the story (and the poem in it) resonated then.
Okay, a stretch for HN, but: singer-songwriter Silvana Estrada named an album released last year Vendrán Suaves Lluvias (meaning There Will Come Soft Rains). She talked about how she and her brother read The Martian Chronicles as kids and she remembered the Sara Teasdale poem quoted at the end. She said she composed the songs at a difficult time in her life and, I guess, something about that image in the story (and the poem in it) resonated then.
In a world with only LLMs doing the day-to-day of proving, you still want more than just proofs dumped out as soon as they pass adversarial review or formalization. The first proof code that passes checks may be a mess that's hard to build on; the path to a result, including failures, is full of interesting stuff; naming, generalizing, linking, and organizing things are tasks that move us from today's raw material to tomorrow's future directions.
Folks get this about code: "it works" isn't the same as "it's good." We knew it before LLMs, out of practical necessity as projects became hard to build on.
An odd thing to me is it would not be that big a concession for the labs to openly talk about the difference between the math artifacts they're releasing and what mathematicians do. It's analogous to the Claude's C Compiler post noting it wouldn't replace a prod C compiler. They could talk about paths from a rough initial product to 'production' math, say they hope future models will continue to improve as math collaborators and expositors, and so on.
For the compiler, the gaps would be trivially obvious to their customers, so it was an obvious call to acknowledg them. With their math output, the difference between a proof dump and the kind of well-written, contextualized mathematical program the community pursues is apparently subtle and deep enough the companies can't get themselves to acknowledge there is any difference. So the companies self congratulate and then are yelled at on the Internet instead.
(Ant seems to have wised up a tiny bit about this compared to OAI, and e.g. Ant handed a recent result to some experts in complexity theory to understand and refine and publish rather than just dumping a Claude-written PDF.)
And yes the drug discovery piece was weird. There are good relevant points: it'd be good to understand pharmaceuticals better (helps us find others, understand side effects, etc.); when we get a mystery result, it's worth effort to try to work our way to proper understanding; anything that could help us understand (reasoning etc.) shouldn't be hidden. But as presented it's both not a lot like math and accidentally a lot like those "would you choose..." questions that always get so much engagement on social media.
reply