Won’t happen unless the thing is implemented in lean4.

Proving something is correct doesn't automatically make it obvious though. For it to be obvious it needs to either be intuitive or it needs to be (reasonably) simple