Mozi Lean Copilot

English | 简体中文

Facilitate formal proof writing in Lean 4 through human-machine collaboration.

Demo.mp4

Quickstart

1. Make sure you have already installed Github Copilot Chat in your Visual Studio Code.
2. Download the VSIX package from the release page and install this extension.
   • Open VSCode
   • Go to the Extensions panel (Cmd+Shift+X or click the Extensions icon in the sidebar)
   • Click the ... menu at the top right corner
   • Select "Install from VSIX..."
   • Choose the mozi-lean-copilot-x.x.x.vsix file
3. Toggle Github Copilot Chat by Ctrl+Shift+i.
4. Type @mozi /settings in the Copilot Chat, insert your api key Mozi-lean-copilot: Api Key field. You are all set!

Features

Currently, Mozi provides 2 commands in writing Lean proofs:

1. /prove: Place your cursor after a Lean theorem statement and type @mozi /prove in the Copilot Chat input box. Mozi will try to generate proof for the theorem.

   Example usage:

   example (m n : ℕ) (h : m ≥ n) :
       card (range n ∪ (range n).image (fun i ↦ m + i)) = 2 * n := by
     /- place cursor here -/sorry

2. /fix: Select a block of proof code that contains errors, and type @mozi /fix in the Copilot Chat input box. Mozi will attempt to fix the errors in the selected proof code.

Configuration

Mozi can be configured through typing the @mozi /settings command in the Copilot Chat input box.

The following settings are available:

• Use Remote Verifier (Default to false): Enable or disable the use of a remote Lean verifier service.
  • true: send proof obligations to the self-hosted remote service for verification.
  • false: use feedback from your local Lean LSP(Language Server Protocol) server.
• Prove Mode (Default to advance):
  • Basic: Rely only on compiler errors and warnings from the Lean to guide proof generation.
  • Advance: Utilize additional information from LeanSearch to enhance proof generation.
• Max Attempts: Set the maximum number of attempts Mozi will make to generate proof or fix errors.

Known Issues

• Remote verifier service may not be stable. If you encounter issues, please try switching to local verification by setting Use Remote Verifier to false.