3 ms·
The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic
by kccqzy 1mo ago
The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.
- Smaug123 1mo agoYou don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.
- make3 1mo agoInteresting. Indeed, proving theorems that are stronger and more general "accidentally" than what you really need is not a bad thing.