Hacker News Reader

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?

maybe it will be an answer that entices them to understand more :)

Yes