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

I have always wanted to learn tactics writing in Lean. But for whatever reason, none of the tutorials that exist online have been helpful. I suspect that the best way to learn to write tactics to play around and modify the existing ones. I came across this short, 4-page tactics tutorial that look . . . Read more