> the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find
Kempe's reduction technique, on which the eventual proof still depended (at least spiritually? I think?), did contain true insight with reach beyond the original problem statement (e.g., Chaitin/register allocation).
I submit that "clever way to soundly reduce to finite set and check" is itself probably one of the more important types of insight in mathematics. Actually, all of my favorite mathematics, from an aesthetic perspective, has exactly this flavor. That's down to taste, of course, but it is sort of a fundamental/powerful move in modern mathematics. The beauty of that insight can only be appreciated once you're willing to accept that boring case checking is tractable.
In that sense, the FCT gave us two really important insights -- first some profound insight from Kempe then an equally profound insight about the role of computers as a bicycle for human thought.
Kempe's reduction technique, on which the eventual proof still depended (at least spiritually? I think?), did contain true insight with reach beyond the original problem statement (e.g., Chaitin/register allocation).
I submit that "clever way to soundly reduce to finite set and check" is itself probably one of the more important types of insight in mathematics. Actually, all of my favorite mathematics, from an aesthetic perspective, has exactly this flavor. That's down to taste, of course, but it is sort of a fundamental/powerful move in modern mathematics. The beauty of that insight can only be appreciated once you're willing to accept that boring case checking is tractable.
In that sense, the FCT gave us two really important insights -- first some profound insight from Kempe then an equally profound insight about the role of computers as a bicycle for human thought.