4 ms·
I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine
by kevinbuzzard 5y ago
I'm not quite sure what you're asking about. I'm saying that we can't yet take the Wiles and Taylor-Wiles proof of Fermat's Last Theorem, feed it into a machine, and get a Lean proof of Fermat's Last Theorem.
- wolverine876 5y agoI think the GP might have been responding to the GGP, not to your statement in the article.
- GPerson 5y agoHi Kevin, Yes, I was responding to the person who said “we're closer to this than people realize” hoping to learn what they had in mind.
- throwaway81523 5y agoI remember asking Bob Solovay whether he thought Wiles' proof of FLT was within reach of formalization and he said something like: it is probably 20 years away. It may have been 20 years since I asked him that, and seeing this recent work with Lean makes me think FLT might also be doable, which would make Solovay's guess just about spot on.