I have an interest in proof reduction. If in the final theorem of a proof, some variables are filled in, then the proof might be reduced to a simpler proof. If all variables are filled, then (often) the proof can fully reduced. I am interested in examples were proof reduction is not possible.
Suppose we would encode Wiles proof in a formal logic. Does the proof reduce if you fill in the values for $a$, $b$, $c$ and $n$?
Suppose we take $a = 11$, $b = 14$, $c = 16$, $n = 3$, then a fully reduced proof would look like this:
$0 \neq 21 \Rightarrow 4075 \neq 4096 \Rightarrow 11^3 + 13^3 \neq 16^3$
If it is not possible to reduce Wiles proof step by step with filled in values, why not?
I don't know much about Wiles proof, but my question is about logic and proof reduction. If you take the Four Color Theorem, then if you a particular planar graph, then you will end up with a graph that is colored with 4 colors.