Jon SterlingMar 17

Regarding Leo’s post, it was in poor taste but no poorer than anyone who knows him has come to expect. My comment is that I bet Lean is inconsistent too. I don’t know exactly where and how, all I am saying is that I don’t doubt it. These are very sophisticated pieces of software.

In fact, I don’t doubt that those working in the trenches of the FRO could point to some dark corners and examples of unpublicised sources of inconsistency.

This isn’t to dunk on Lean. Bugs can happen, and having a small kernel is a good way to limit their scope! But there are many ways for assurances to fail and this can happen inside and outside the kernel.

Show threadJon SterlingMar 17

I am also not too impressed by the existence of second-party checkers in the context of a language that lacks decidable type checking. Because something has to give, these checkers will be (necessarily) incomplete in one way or another, most likely each in different ways. This is because lean’s failure of completeness of conversion almost certainly manifests in heuristic ways that are not predictable or replicable…

For a fail safe checker to provide confidence, it needs to be complete. This is not possible with Lean’s core language as designed, and it will not be possible for Lean itself until they find new leadership.

Show thread⏚ Antoine Chambert-LoirMar 17
@jonmsterling Would you please give a link to Leo's post?
Show threadJon Sterling
@antoinechambertloir https://leodemoura.github.io/blog/2026-3-16-who-watches-the-provers/
Who Watches the Provers? — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

Mar 17 at 9:52pmWeb