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.