OK. I've translated the (correctness) requirements of LeetCode No.22 to Lean, and ask Claude Code to both implement a solution and prove it.
@_torayuri3 notes8 replies0 tags, 1 user following1 followeri create thingsenter to followenter to reply
In the first attempt, Opus 4.7 successfully completed it and proved it. However, the solution is to enumerate all possible space and .filter out anything that doesn't qualify my definition, which is obviously not ideal (if cheating is too harsh).
@_torayuri3 notes8 replies0 tags, 1 user following1 followeri create thingsenter to followenter to reply
I can't think of a good way to also prevent that kind of solutions and ended up prompting "please don't enumerate and filter". Opus 4.7 then reimplemented and proved the backtracking algorithm.