5 ms·
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
by 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 agoKevin 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 agoIs any piece you've seen in good enough shape to be in a Lean library?
- wyager 12d agoI 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 agoIt indeed does, this is a very good point I haven't thought about in the reverse direction.