I think an interesting problem, perhaps even more interesting problem, would be ...

chvid 20 days ago | parent | context | favorite | on: Fermat's Last Theorem in Lean 4

I think an interesting problem, perhaps even more interesting problem, would be the shortest / most concise / easiest to understand (formally verifiably) proof.