Bu's Blog: AI and the future of Math and TCS
There is a very good video by Terence Tao from the last ICM regarding the use of AI, and how he believes it will transform mathematics (and theoretical computer science).
Terence Tao's Invited Talk on ICM
The bottom line: We need to move beyond the mindset of "it has been proven (somehow)" where we just possess a formal proof (he calls this "proof verification"). Instead we should focus on questions such as:
- Can we understand the (formal) proof?
- Is it communicable?
- Is it publishable?
- Is it suitable for teaching to students?
He presents the following hierarchy for scientific work:
He argues that scientific practice in our field must shift away from the initial two phases (which AI is becoming increasingly powerful). He implicitly reaffirms a clear commitment to scientific formalism. He states that someone who possesses a proof but cannot explain it cannot truly be the author of that proof.
This aligns perfectly with my own experience: I never publish "first-shot" results. My doctoral students and I take the time to repeatedly refine our initial formal proofs, ultimately shaping them into a form suitable for inclusion in the AFP (Archive of Formal Proofs). In one extreme case, we reduced a 2,200-line proof to 200 lines; it now runs in 20 seconds during every regression test. Rumor has it that the Lean proof of Fermat's Last Theorem (FLT) could be condensed from 11 million lines of code to 1 million or less --- a task that, from what I hear, is currently the subject of significant effort. That's the truly scientific work.
In other words: "first-shot" results may be reassuring, but they are not necessarily scientifically significant. For people who are content to settle for “proof (sketch) generation” in their papers and books, all of this is, of course, terribly inconvenient.
Bu