jaykru

The exact meaning of the "don't train on my data" checkbox is pretty hard to pin down.

I think the concern is that it could be seen as minimizing the harm done to those affected, but I personally think this is kind of a hypersensitive overcorrection :P

Would you rather ancient issues to which our bodies have apparently adapted or new issues we haven't yet had time to adapt to? I'm not sure on the answer myself but it doesn't appear as clear cut as no worms => no issues.

To boot even if you skip the free models, you could probably do a year's DIY assistance with 50 cents worth of GLM or Deepseek tokens. And the really costly jobs are ones where an AI assistant won't really help since, shockingly, most of the cost is hours of labor which you would have to do yourself.

That's super interesting. I wonder if you've tried optimizing for type-checking duration of a richly dependently typed program and gotten viscerally nicer code out of that.

Curry-Howard doesn't buy you any shortcuts to capability. Surely no expense has been spared in training models to write good (well modularized, robust, generic etc.) code, and yet they still write slop (poorly structured, overfit to specification gaps, etc.) We see the same sloppish habits in their mathematics, perhaps transported along the CH iso. So "train[ing] agents to write better proofs" seems to me like a grand challenge problem for AI research, just like getting them to write good code. It won't be solved just by noticing that the two problems are isomorphic: we'll keep getting models that are a little better at grinding out proofs, hence a little better at grinding out programs, but the abstraction wall won't magically drop in either world just because the same limited behaviors can be transported along CH.

From the appendix [0]: "The proofs written by agents are just as 'good' as any other proof of the same theorem, in that they prove the equivalence theorem. However, it remains to be seen whether agents can scale this verbose proof style directly to more complex programs. Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles. If that is the case, how can we help agents discover and introduce the right abstractions to reduce this complexity? Does this require input from expert proof engineers, or can we extract common principles that can guide agents to discovering good abstractions that will enable scalable proofs?"

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...

Here are a few that one might construe as panicky/aimed at soliciting anti-competitive regulation:

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

the autoformalization could be proving a subtly distinct result; if the area is not in mathlib already there's likely not a good reference theorem specification to use for a comparator check. or it could be exploiting kernel bugs. just using a second checker kernel is not enough; there has been an example of a model interpolating bugs across multiple checkers in a single bogus proof.

I kind of feel motte-and-bailey'd here. You began by questioning the value of human understanding in mathematics and I've explained (exactly as you've said) why it is currently on the critical path of outcomes in science and engineering with value to humanity almost nobody would dispute. This new question, where human understanding of mathematics isn't on the critical path of anything, is something I can't argue, in the same way that I can't argue for the intrinsic value or meaning of essentially any human activity without resorting to what amount to basically religious axioms.

this is the term of art in the mathematics community. considering that the vast majority of the results don't come with a typechecking lean formalization, i don't think it's off base at all either.

many of these are not accompanied with leanslop

I wrote something that might answer a bit a few weeks ago: https://dank.systems/posts/2026-09-15-ai-bear.html. Today's slopdrop certainly is challenging my stubbornness, but everything I've seen so far indicates that these (hugely impressive, world historic) capabilities won't extend past verifiable domains. Math yields especially impressive results because it so broad and deep that essentially no person can know of all of its parts; pretraining and deep search capacity is a huge advantage. Gowers has recently written about these capabilities and gestured [0] toward some human capabilities lacking from the current frontier models, though he isn't convinced they won't develop soon. If you assume we don't get a total mathematical superintelligence (which to me seems already sort of AGI-complete) and only amplify the capabilities we have today, it's not obvious to me that we get takeoff from recursive self-improvement, unless you happen to believe that 1) we can clearly specify what AGI or ASI is 2) all of the requisite ideas are out there and need only be combined and/or optimized.

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

The fact that you need to ask "the right questions" is why it's not AGI. A general intelligence should be able to ask of its own volition the interesting questions required to advance its goals.

I think the central problem with that line of reasoning is that it supposes we are already living with AGI. Even the latest PR from Anthropic admits that we are not [0] there yet. If we don't have AGI capable of integrating and employing the mathematical results produced by an artificially superintelligent theorem prover so that they become useful to the rest of science and engineering, we will need humans to do at least some of the work in mathematics. Moreover if we freeze current AI capabilities today, "digestion" probably doesn't scale, so mathematical research will probably end up AI-assisted in ways not far off from what we're already seeing in the sciences.

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

Wolfram gives a very important and sober take on the present state and future of pure math. I came away with the following key takeaways:

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...

> You need to unambiguously describe what you need to be built

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.

Hi! Thanks for the feedback. I've added an orthography toggle for those who prefer a more conventional look.

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!

That is the point I was making, that auto mode is itself a guardrail on top of the model (and not a perfect one.) auto mode seems to cover merely actions the model could take that are clearly bad, like wiping your disk, using an overly privileged context to complete the task, etc.

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.

why don't anthropic and openai ship yolo mode by default?

yes, huge for pure math and activities that look like it.

Thanks :) I do enjoy and use these things every day and the current capabilities are indeed amazing, just ludicrously overpriced at the frontier.

archive link in case i get hugged lol https://archive.ph/Z4gxF

corrected my comment, apologies for the uncorroborated misinfo.

The cascading outage theory would make sense to me for Claude -> Codex. But Grok and Gemini too?

[actually gemini at least on the web appears to be up, contrary to some reports in this thread]

Layoff note mentions AI => it's not AI

Layoff note omits AI => it's AI

I am onboard with the idea that corporate messaging is typically anything but forthright but I don't see the logic here.

"The average American aged 18 to 34 carries more than $40 thousand in non-mortgage debt across student loans, credit card balances, auto loans, and personal loans, with some estimates go as high as $100 thousand. This is the cohort the Pentagon needs. A federally administered debt-forgiveness enlistment program that fully discharges student loan, credit card, and loan balances after 24 or 36 months of service, and extends the GI Bill, would produce voluntary enlistment at scale."

Never for a moment thought my Subaru would be sending me to die for Israel. How could a patriotic Israeli write deranged dreck like this knowing full well the PR catastrophe the state is experiencing in the United States? It's so beyond the pale that you might even read it as parody.

Wow, that's totally crazy. Does it happen even if you clear out the "offending" memory entries?

GLM 5.3 will probably do your vintage computing work without fuss.