Comment by sweetheart

Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.