Login
You're viewing the discuss.systems public feed.

Replies

  • Josh Chenjoshchen@types.pl
    Sep 10, 2026, 10:00 AM

    "I hope that this will put an end to the worry about large AI formalization possibly abusing kernel implementation bugs"

    I have questions about the huge pile of code and a mess of the proof of False-ity rejection that is formalized by AI and checked by the Lean kernel

    💬 0🔄 0⭐ 0
  • 💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • Josh Chenjoshchen@types.pl
    Sep 10, 2026, 10:23 AM

    @amy I'm taking a bit of time to check I understand how this is actually supposed to work; there's an AI Lean implementation of an interpreter into an internalized set model? I forget what the status of the set model in Carneiro's thesis was

    💬 3🔄 0⭐ 0
  • Amélia Liao 🍊😈amy@types.pl
    Sep 10, 2026, 10:27 AM

    @joshchen i would not waste my time trying to understand this slop superfund site if i were you. even the person who published it hasn't bothered

    💬 1🔄 1⭐ 3
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Sep 10, 2026, 10:42 AM

    @amy @joshchen The point is not the understanding, it is to reassure funders that there can't be any kernel bug exploit in their 13G lines of slop

    💬 2🔄 0⭐ 8
  • 💬 0🔄 1⭐ 10
  • Josh Chenjoshchen@types.pl
    Sep 10, 2026, 12:15 PM

    @mevenlennonbertrand @amy I just want to know whether I will have a tasty meal or die of sodium poisoning with the amount of salt with which I have to take "I declare the summer of AI-found kernel implementation bugs to be over" in Joachim's announcement

    💬 1🔄 0⭐ 3
  • 💬 0🔄 1⭐ 4
  • 💬 1🔄 0⭐ 1
  • 💬 0🔄 0⭐ 1
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Sep 10, 2026, 10:38 AM

    @joshchen @amy In terms of formalisation, it's essentially nowhere last I heard. And in any case even in the thesis inductive types are rather sketched than fully handled

    💬 2🔄 0⭐ 0
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Sep 10, 2026, 12:04 PM

    @joshchen @amy (Although there is some amount of set theory in Mathlib, but I don't think there's anything like a model of type theory there)

    💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Sep 11, 2026, 8:27 AM

    @joshchen @amy Yes! Mario was/is essentially alone on Lean4Lean, and until now he was spending his Lean4Lean energy on the specification of the theory, the checker, and some meta-theory. But I think he would welcome anyone serious who wants to look at the set theory part

    💬 0🔄 0⭐ 0
  • Meven Lennon-Bertrandmevenlennonbertrand@lipn.info
    Sep 10, 2026, 10:40 AM

    @joshchen @amy I think that's the right rough description (with the big caveat that the interpreter I'd not verified, it's more of a "translation validation" kind of thing). I'd like to see what the set model looks like: if it's too much like Lean, this will end up being just a very complicated way to map Lean to Lean itself, without much further guarantees. Although probably at least inductive types are translated away which is a big win

    💬 0🔄 0⭐ 0
  • 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?

    💬 1🔄 0⭐ 0
  • Josh Chenjoshchen@types.pl
    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.

    💬 1🔄 0⭐ 0
  • Naïm Camille Favier 🎃ncf@types.pl
    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?

    💬 1🔄 0⭐ 0
  • Josh Chenjoshchen@types.pl
    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.

    @mildsunrise

    💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0