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?

	▲	sweetheart an hour ago \| parent [-]
		maybe it will be an answer that entices them to understand more :)