Can lean instantiate a state?

Stream: Machine Learning for Theorem Proving

[Your full name]

Hi! I'm from ML and am newbie to lean, to clarify my question, is there a way to draw random, concrete examples from a lean state (where applicable)? Because my inclinations are that LLMs would have a easier time with examples beside abstract theorem states. cheers!

[Jason Rute]

You mean like instantiating some/most/all of the variables in the local context of a goal state? One one hand, this is a metaprogramming question and there are tools like plausable that do that sort of stuff (I think systematically instead of randomly). They probably could be adapted for this use case. But on the other hand, I’m curious what sort of examples you think it would help with.

[Jason Rute]

On a much more extreme level, AlphaProof dreams up conjectures which are variations of the current theorem, often specializing to particular subcases. Then they see in their RL loop if they can solve those cases. I think they just use an LLM to do that.

[Eric Wieser]

I think plausible is mostly random, then has some systematic way to try to simplify counterexamples

[Your full name]

Yes! cheers for mentioning plausible, seems to be exacly what i was looking for.