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".
So humans do/did still have a role to play
I do not think it is a given that humans or algorithms can find such a proof for any given problem.