Discussion: thread for Mozi Lean Copilot

Stream: general

[Yutong Wang]

Discussion thread for #announce > Announcing Mozi Lean Copilot(VS Code): agentic prove and fix

[Alfredo Moreira-Rosa]

Is it using github copilot subscription and selected LLM to run ? Or will it require an additional subscription ?

[Yutong Wang]

Alfredo Moreira-Rosa said:

Is it using github copilot subscription and selected LLM to run ? Or will it require an additional subscription ?

No, it does not. Now we only utilize the frontend of github copilot and no subscription required.

[Nick Adfor]

Unable to install extension 'mozi-lean-copilot.mozi-lean-copilot' as it is not compatible with VS Code '1.88.0'.

[Snir Broshi]

VSCode 1.88 is 2 years old