3 ms·

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

• nasretdinov 4mo ago
  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