alt Hacker News> To be clear, I haven’t fully verified the proof; I worked through it with Claude Fable and it passes the sniff test, but fully digesting it will take a bit more energy than I have right now.
As predicted, we no longer need mathematicians for math; the math is being both generated and read by models. We're in for some exciting times, when the pace of mathematical advance can run faster than the constraints of human brains.
We definitely need mathematicians to understand it and verify to us that the math is correct. And it takes a mathematician to even talk to the AI in a way that will be useful. There is no way I could personally get Claude Fable or Opean AI GPT 6 to generate a proof of Fermat's Theorem in LEAN. It actually take mathematical skills. And real depth to understand the work.