Lean _is_ code. FLT cannot be proven by exhaustion because it's domain is an infinite set: the natural numbers above 2.
If they’re asking that kind of question, do you think this answer will help them understand anything?
alt Hacker News
If they’re asking that kind of question, do you think this answer will help them understand anything?