The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.

▲

omnicognate 2 hours ago | parent | next [-]

Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)

	▲	whatshisface 2 hours ago \| parent [-]
		Maybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.

▲

nowittyusername 44 minutes ago | parent | prev | next [-]

I don't think it will be a problem for long, as AI systems evolve they will be able to find those elegant solutions and explanations for you in due time...

	▲	cat-whisperer 13 minutes ago \| parent [-]
		I doubt that. I don't think AI are trained to find elegant solutions, they are trained to find solutions. if you look at the things that OpenAI published, so seem to be micro improvements riddled with chaos. They are better solution, but they aren't drastic. I have noticed this with autoresearch too, the solutions and improvments that you get are incremental and not groundbreaking. Humans, have a way find elegant solutions and also seem to solve that problem. Then again, beauty is in the eye of the beholder, and I might be wrong.

▲

utopcell 2 hours ago | parent | prev | next [-]

> "The problem of the proof was that we knew that FCT was true"

Citation needed.

▲

fhdkweig 2 hours ago | parent [-]

That was terrible phrasing. I meant "The problem with the proof was that although it showed that FCT was true, the proof did not explain why".

	▲	keybrd-intrrpt 23 minutes ago \| parent \| next [-]
		> the proof did not explain why So humans do/did still have a role to play
	▲	dunham an hour ago \| parent \| prev [-]
		Yeah. On a similar note, without the computer aspect, I once had a prof tell me that he did not like character theory. If I remember right, there you calculate some numbers from a group and can prove some properties about it. But you gain no understanding of why those properties hold.

▲

aaron695 an hour ago | parent | prev [-]

[dead]