Reading
- Can Opus 4.6 do Category Theory in Lean?: "[W]hen Anthropic dropped the new Opus 4.6 model, I wanted to know: can it actually write proper Lean 4? Not toy examples. Not theorem two_plus_two : 2 + 2 = 4 := rfl. Real proofs with real proof obligations, the kind where you need to wrangle naturality squares and coherence conditions and the elaborator is fighting you every step of the way. The beautiful thing about a proof assistant is that the answer is ground-verifiable. You don't have to squint at the output and wonder if it's subtly wrong. Either lake build passes or it doesn't. The kernel doesn't care about your feelings. The short answer is: yes, kinda mostly. But the longer answer is more interesting."
Tags:
ai
model
Last modified 03 November 2026