LeanCopilot is a newly-released repository for using an LLM to complete proofs in Lean. I intend to install it this week and try it out.

This resolves YES if I use LeanCopilot suggestions at least twice in the month of March.

I will not bet.

Some potentially helpful details about my LLM usage: I have used GitHub copilot and I really like it, particularly how it just automatically provides suggestions without my asking. I don't really use other LLM tools regularly. I have tried out rw_search, and I found it sometimes helpful, though I haven't used it frequently.