MathCopilot

You mark the claims in your LaTeX paper that you want checked. MathCopilot translates each one into a formal statement in Lean 4, tries to prove it, and reports the outcome next to the claim in your compiled PDF.

MathCopilot verifies all of the mathematical reasoning in your document using Lean. For background results invoked or cited in the paper that are not already in Mathlib or Tau Ceti, we double-check the statements with web search and then take them as formal axioms. Our pipeline uses several layers of adversarial review to make sure the formal statements in Lean match the intent of your document.

• To speed up refereeing: submit a formal verification to the journal along with your paper.
• To catch errors in your paper. MathCopilot is especially good at catching missing hypotheses and assumptions.
• To check that a long LLM-generated argument is valid before you invest the effort to understand it.
• To rely on an LLM-generated argument for a fact you need, without reviewing it in detail yourself.

An Overleaf project whose owner has a paid plan, or a LaTeX document in a GitHub repository.

Add \usepackage{mathcopilot} to your main LaTeX file, after \usepackage{hyperref}. Put each claim you want formalized in a theorem-like environment (theorem, lemma, proposition, definition, …) and label it with \autolabel{my_id} instead of \label{my_id}.

No. It never edits your LaTeX documents. It adds two things to your project: the file mathcopilot.sty, and a math_copilot/ folder that holds the Lean code and the results. MathCopilot manages that folder, so anything you change in it by hand is overwritten on the next run.

Projects are processed overnight. The next time you compile (after pulling, if your paper is on GitHub), each marked claim shows a green checkmark or an orange [!]. The Lean files and a progress summary are in the math_copilot/ folder.

We copy your project to our server to run the pipeline, and the pipeline sends text from it to third-party AI model providers. The privacy policy says what we store, who receives it and how to remove it. If your work is under a confidentiality agreement, read the policy before you connect the project.

Choose Disconnect next to the project on your dashboard. We stop processing it, and our copy of it is deleted about 30 days later. The files MathCopilot added to your project stay there until you delete them. To delete your account, email [email protected].