7 ms·

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries. My experience is that it takes

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries. My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)

Jhsto 12d ago
My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.
- black_knight 12d ago
  Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.
  - refulgentis 12d ago
    Is any piece you've seen in good enough shape to be in a Lean library?
- wyager 12d ago
  I believe Lean supports a signature search mechanism. E.g. Haskell has Hoogle, Lean has Loogle. So in many ways it's actually easier to search for "library" code than in most languages, because the type tells you everything you need to know and you don't need to care about the implementation.
  - Jhsto 11d ago
    It indeed does, this is a very good point I haven't thought about in the reverse direction.
kmoser 12d ago
Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?
- ezwoodland 12d ago
  You can only do so in another framework that might itself have bugs. Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean". The kernel does have bugs sometimes.
  - DoctorOetker 12d ago
    I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.
- michael0church 12d ago
  [dead]
  - DoctorOetker 12d ago
    would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
    - dwheeler 12d ago
      Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
  - torginus 12d ago
    So is there a chance that some of these AI-discovered proofs are actually Lean exploits?

Jhsto 12d ago

My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.

black_knight 12d ago
Kevin might not care, but I care more about building the foundation for future proofs and human understanding than I do about this particular result.
- refulgentis 12d ago
  Is any piece you've seen in good enough shape to be in a Lean library?
wyager 12d ago
I believe Lean supports a signature search mechanism. E.g. Haskell has Hoogle, Lean has Loogle. So in many ways it's actually easier to search for "library" code than in most languages, because the type tells you everything you need to know and you don't need to care about the implementation.
- Jhsto 11d ago
  It indeed does, this is a very good point I haven't thought about in the reverse direction.

kmoser 12d ago

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?

ezwoodland 12d ago
You can only do so in another framework that might itself have bugs. Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean". The kernel does have bugs sometimes.
- DoctorOetker 12d ago
  I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.
michael0church 12d ago
[dead]
- DoctorOetker 12d ago
  would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
  - dwheeler 12d ago
    Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
- torginus 12d ago
  So is there a chance that some of these AI-discovered proofs are actually Lean exploits?