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 [LeanDojo](2023-09-04 leandojo.qmd) somehow and I don’t understand the difference between the two. Unfortunately, I do not know enough about LLM and AI to tell if this is actually good or just hot gas.