Alba 🌸 :v_pat:mildsunrise@tech.lgbt
Sep 10, 2026, 1:17 PM@joshchen I feel dumb but, uh, slop aside isn't "Lean proof that our Lean checker is consistent" bad news per Gödel's second incompleteness theorem?
Replies
Sep 10, 2026, 2:44 PM@mildsunrise AFAICT, the approach that this work wants to take follows that of a standard relative consistency proof in mathematical logic: postulate enough inaccessibles+whatever else you want, build a nontrivial "model of Lean" and define an interpretation function of Lean theories (collections of definitions and statements) into the model. Incompleteness does not forbid this and is not the issue.
The unsubstantiated leap is (to oversimplify) to take this "proof" of relative consistency via model existence, and extrapolate that to consistency of the implementation of the Lean kernel. I'm not aware of anyone in the field who seriously doubts the existence of models of "idealized Lean", insofar as such a thing exists separate from its official implementation.
Sep 10, 2026, 6:24 PM@joshchen @mildsunrise i hate to quibble about the exact modalities of the sloppers' imposture, but that's not what they're claiming, right? afaict they claim to have vibecoded a separate implementation of lean and vibeproven that it is sound for their set-theoretic semantics?
- Sep 11, 2026, 7:58 AM
@ncf Mm given that the syntax and whatever "extra work" the checker does is also all implemented in Lean, that just about boils down to the content of my first paragraph with extra steps, no? Unless I misunderstood something about the setup. But I also cba trying to further make precise what the creators cba to properly document.
zwarichzwarich@hachyderm.ioSep 10, 2026, 9:06 PM@mildsunrise @joshchen They assume the existence of a model of ZF + ω inaccessibles:
https://github.com/leanprover/con-leche/blob/master/OVERVIEW.md#7-the-set-theory-assumption
This is similar to MetaRocq assuming that PCUIC is strongly normalizing.