I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.

I'm probably wrong, but what's the point of throwing away all skepticism?

Here's a recent example of an AI exploiting a soundness hole in Lean in a paper purporting to have solved the Collatz Conjecture.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

There's also a fairly well known incident where the Lean formalization of the Riemann Hypothesis in Mathlib was incorrect.