Some mathematicians have observed a similar pattern in the recent LLM proof drops, leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics. The sort of proofs done in formal verification are a pretty interesting litmus test for LLM reasoning since the systems considered aren't necessarily on distribution (compare with math where the "systems" and structures worked with, and proofs about them, make appearances in thousands of individual books) so the advantages in broad domain knowledge pretrained LLMs have over humans doesn't really buy you much. IMO this observation from Anthropic/Theorem lends more credibility to the convex hull hypothesis.

[0] https://www-cdn.anthropic.com/files/4zrzovbb/website/6867ead...

https://www.anthropic.com/research/self-replicating-ai

https://www.anthropic.com/research/glm-5-3-and-the-spread-of...

https://www.anthropic.com/research/distillation-defenses

[0] https://dank.systems/posts/2026-09-15-ai-bear.html

[1] https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-a...

[0] https://www.anthropic.com/research/claude-shaped-science

1. An essential goal of mathematics is human understanding. The computation of proof terms doesn't necessarily enrich human understanding. The proof of the four color theorem result is a good example, and formal verification/SAT solving gives many more: these are results that can be trusted up to our trust in the system used to produce them, and they can be used in practice, but they don't necessarily enrich our understanding. Imagine a computer with near infinite proof search powers set loose with the current human definitions, theorems, and understanding of mathematics. Suppose it constructs a proof for a new theorem at our mathematical frontier. The shortest such proof in terms of currently understood definitions and concepts could be so long and mechanical that the entire lineage of humans until the end of the universe could not finish reading it. So though it overlaps with the activity of mathematicians, this type of computational proof search is not mathematics as such. This is an important distinction that many people do not seem to grasp and some dismiss as cope.

2. The human activity of theory building, rendering otherwise monstrous proofs like the one I discussed above into light conceptual arguments a person can understand, appears at this time out of reach of models. Maybe they will do this in the future, but it is not yet the case. Human theory building drastically compresses the spaces of theorems and their proofs: this is why great theory builders like Groethendieck are so important to the field; grinding has its value too, but runs up against computational limits in both humans and computers. These limits are collapsed by the conceptual shortcuts created by theory builders.

Gowers has a nice and arguably better-grounded article on the mathematical capabilities of recent LLMs that I think is enlightening to read alongside Wolfram's bird's eye view of the implications of those capabilities: https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-a...

In the limit this can be as complex or more complex than just writing your program to begin with. If you actually care about your implementation details, your specification will balloon to encode all of them.

I will add that I'm not very happy with the readability of my site overall at the moment; if anyone has font or other recommendations for style tweaks to make I'd love to hear them!

I recently tasked a GPT model in Codex with implementing part of a new architecture I'm working on. I gave it a very detailed spec and the code it produced looked pretty reasonable and passed my tests. It even did exceptionally well in my evals, so I excitedly declared victory to a few friends. The next day after more careful review I found that the architecture implementation was totally correct, but the model had slipped a one line change to the observation encoding of the RL environment I was prototyping against. The encoding change made the learning problem essentially trivial; the architecture itself, I later realized, had a major flaw that was revealed by returning to the natural encoding.

This is the type of reward hack that is hard to paper over with easy guardrails like auto mode and even harder to specify out. It's also the type of thing a reasonable human wouldn't do unless they were intentionally trying to deceive you.

Comments URL: https://news.ycombinator.com/item?id=49715927

Points: 496

# Comments: 653