Comment by Jblx2
10 hours ago
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago:
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
10 hours ago
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago:
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
True, .. and. In this case, the original proof is considered rigorously checked, so finding a bug in the kernel would be nice to know about, but in my opinion would not take away from the accomplishment (FLT in lean using agents) nor the many benefits of getting these mathematical objects formalized and usable in Lean in the future.