That’s what they do usually I understand - llm generates proof in lean, and proof checker proves.