Not a lot of mention of AI for CS, even in 2002. What about (2080+, P/=NP, proof techniques completely opaque to humans). And by that I don't mean mechanical exclusion of special cases like for map-coloring. As mentioned already, there's like a handful of people that understand the FLT proof, that situation is unlikely to improve.