[kevinbuzzard]

I highly doubt that the proof will get small enough to fit into a margin, but history shows that it's not at all unreasonable to expect simplifications/generalisations of the argument to come out of a formalisation (for example this happened with the Liquid Tensor Experiment, where dependence on stable homotopy groups of sphere was completely removed from the argument). I think it is unreasonable to expect that at the end of an FLT formalisation there will be no mention of elliptic curves, modular forms, Galois representations etc (the standard tools used by Wiles to prove the result in the 90s and which have themselves been simplified and generalised by mathematicians such as Taylor and Kisin since then). And you'll need quite a big margin to get all that stuff in.