> I’ve had the experience quite a few times now: I try to autoformalize something, and an AI will tell me “I did it; look, the proof checks out!” But, actually, in some sense it cheated: instead of formalizing what I intended, it found a (sometimes very squirrely) way to interpret what I asked so that it could successfully prove it. It’s often very hard to tell, though, that this is what happened—not least because the formalized versions of things (say as expressed in popular proof assistant systems) tend to be very low level, very verbose and very hard for us humans to understand.

This has largely been my experience in programming, too. Often when given a broad objective within an existing code base, even the frontier models seem to stand up a half dozen tests proving compliance and then add 3 new branches solving for those specific tests alone. My best guess is that our code base is quite far out of the distribution (and not for just good reasons). The agents are thus reduced to these tactics rather than extending and refactoring well known abstractions.