We can't really formalise what theorems humans would care about, so I'm afraid this is hard to answer rigorously. But there are some theorems many people care

We can't really formalise what theorems humans would care about, so I'm afraid this is hard to answer rigorously. But there are some theorems many people care about and they don't have any known short proofs (e.g. Fermat's Last Theorem).