“The raw output of ChatGPT’s proof was actually quite poor. So it required an expert to kind of sift through and actually understand what it was trying to say,” Lichtman says. But now he and Tao have shortened the proof so that it better distills the LLM’s key insight.

This tracks with what I have seen regarding AI. It looks superficially awesome, but when you start to analyze its output it has a lot of holes that require someone trained in the art to fix. You know, someone with years of experience, and who got that experience without the benefit of AI shortcuts.

What happens 10 or 15 years from now, when all the current crop of experts are retired and all the experts who could have curated the AI output had to spend all that time as baristas instead because the AI took all of their entry level jobs?