Is the intention to grow this repo into a useful tool?

[SamPruden]

Is this repo/organisation only intended as a snapshot of the work in the paper, or is there interest in growing this into an open source project and a useful tool by doing things like integrating this into Lean as a tactic?

This is very cool by the way! I'm excited to finally have an open source model doing this that I can start playing with without prohibitive compute requirements, and the premise retrieval is something I've wanted to see tried / try myself for a long time!

[yangky11]

Thanks for your interest in our work! We're currently working on tools that can be used locally in Lean's VSCode workflow (The first step would be to enable running our models locally in Lean). I'm not sure if the results will be integrated into this repo. More likely, it will be a separate repo within the lean-dojo Github organization that interoperates with this repo.

[yangky11]

We will open-source the WIP once we have an initial prototype, and we definitely welcome contributions from the community! We're curious about any specific functions that can support you in exploring those ideas. According to our current plan, we want to be able to wrap machine learning models trained in Python into Lean (possibly through Lean's FFI). As a first step, we'll focus on models that take strings as input/output. If successful, it enables applications such as

• Tactics that call machine learning models to generate tactic suggestions.
• Tactics performing proof search by integrating aesop and machine learning
• Tactics performing premise seletion

[SamPruden]

That all sounds great!

One thing that might be worth doing is having a nice way to get a list of all identifiers currently in scope, and a little more syntax info about the partially generated code. This could be used to accelerate inference, because we would probably find that it's quite common that there's actually only a single valid next byte, which can be filled in without consulting the model. This could also be used to force the model to only generate valid identifier names, which may help search times significantly if it has a habit of hallucinating lemmas.

I have no idea how practical it is to actually get that information out of Lean.

[yangky11]

It should be straightforward to get the list of all identifiers from the Environment (accessible in the CoreM monad) in Lean 4. Alternatively, you could utilize Lean's language server to generate autocompletions.

[SamPruden]

Yeah I thought about autocompletions, but I wasn't sure if those were actually complete, but that would be ideal if they are. Culling would need to be conservative about not removing valid candidates.

Apart from this type of thing to accelerate search with a view towards more practical RL, I believe everything else that I want to do would already be covered by what you're planning. Most of the fun I have (tentatively) planned happens on the model and custom data side of things.

[yangky11]

@SamPruden https://github.com/lean-dojo/LeanCopilot

[yangky11]

We released Lean Copilot for LLMs to suggest tactics, search for proofs, and select premises directly in Lean: https://github.com/lean-dojo/LeanCopilot