Make it a more Copilot-like experience

[BoltonBailey]

This is very cool, I have successfully installed it and will be trying it out!

One thing I would like is the capability to have a more GitHub Copilot-like experience. If I could have this automatically and invisibly insert search_proof whenever my cursor is in a place where a tactic needs to be written, then have it show optional completions if and when the model finds a proof, that would be very convenient.

It would also be nice to have it in the form of a VSCode extension so that I don't have to install it/ensure compatibility for every repo I want to use it in.

[Peiyang-Song]

@BoltonBailey Thank you for the kind words and the suggestions! We decided to stick to the Lean frontend for displaying suggestions so that various additional information, most importantly the Lean environmental feedback can be displayed nicely (currently via different coloring). The idea of wrapping up Lean Copilot in a VSCode extension sounds interesting. While we may not have the extra bandwidth for the engineering in the near future, we certainly welcome contributions!