I disagree on K4. People are claiming they solved it every day using AI but it doesn't pass the verifier. I would be shocked if it was ever solved by AI.

I personally think it is a weird OTP (effectively). We have the book but the algorithm is so unclear it could be anything.