Why re-formalise Fermat's Last Theorem instead of doing something new? It's obviously an improvement, but it's an odd thing to boast about as opposed to a novel formalisation or proof.