Comment by mswphd
10 hours ago
I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.
Of course, there's a possibility but it exists everywhere but there's no sign till now that it has. Same with openai's proofs.