LLM-powered tactics

Stream: Machine Learning for Theorem Proving

[Louis Cabarion]

There are several promising models aimed at automatically filling in sorrys.

Which of these can be interacted with directly in the development environment via tactics?

More specifically, I'm looking for solutions similar to reap, which after being added via lakefile.toml provides the LLM-powered tactics reap, reap?, and reap!.

What are the current recommended options?

[Kim Morrison]

As far as I'm aware nothing else that is publicly available is as straightforward to install as reap.