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

Replies

  • 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