search

wiio12 / LEGO-Prover

Code for the paper LEGO-Prover: Neural Theorem Proving with Growing Libraries
MIT License
54 stars 4 forks source link

Final skill library? #4

Open ikb-a opened 2 months ago

ikb-a commented 2 months ago

Hi! Firstly, great paper and a big thank-you for releasing the solved theorems and LLM inputs/outputs as requested by https://github.com/wiio12/LEGO-Prover/issues/1; good stuff!

I wanted to ask, will the 20k learned skills be released? I don't think they're in the repo (presumably barring the subset that are used in the prompts that successfully created solutions), and I was hoping to take a closer look at the skills the system had learned.

Thanks!

ikb-a commented 2 months ago

A followup request: in addition to the full library, would it also be possible to release the lineages of the lemmas? i.e., how they were created and what other lemma(s) or pending request(s) were involved in their creation. Thanks again!