[baq]

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

[nasretdinov]

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