Towards Large Language Models as Copilots for Theorem Proving in Lean