I came across two LLM based tactics for Lean llmstep: [L]LM proofstep suggestions in Lean LeanInfer: Neural Network Inference in Lean 4 They both use [LeanDoj . . . Read more

This was posted a while back on the Lean Zulip: LeanDojo LeanDojo: Theorem Proving with Retrieval-Augmented Language Models According to their description, LeanDojo is an open-source Lean play . . . Read more