Fascinating. Given that there's no Lean proof and assuming everything in the paper is correct, can the problem be considered "solved"? Does the paper include a "non-Lean" proof?