text: On the other hand, proof assistants allow verifying all details that cannot be given in a hand-written proof, and provide certainty of the correctness of long proofs such as that of the Feit–Thompson theorem.