One more trick: They look for both proofs and disproofs. So even if they failed the formalization and created a "wrong" theorem, it's just another task.