Who we are

MathCopilot is part of Autoformalization for the Working Mathematician, a research project run by Daniel Halpern-Leistner in the Department of Mathematics at Cornell University and supported by a DARPA expMath grant. “We” means the project's team. You can reach us at [email protected].

What we collect

• Access requests. When you request access we store your email address, name and institution.
• Your account. We store your email address, any additional addresses you add, your name and your institution.
• Project connections. For each project we store the name you give it and how to reach it: for Overleaf, the project ID and your Overleaf Git token; for GitHub, the repository name and the installation ID of the MathCopilot GitHub App.
• Your project's content. To run the pipeline we clone the whole connected repository to our server, including files you did not mark for formalization. We keep that copy together with what the pipeline produces from it: the Lean code, intermediate drafts, caches and logs.
• Run records. For each run we record when it happened, whether it succeeded, how many claims it handled, and how much AI model usage it cost.
• Server logs. Our web server logs each request, including your IP address.
• Email you send us. Mail sent to an @mathcopilot.org address is forwarded to a member of the team.

We set one cookie, named session, which keeps you logged in for 30 days or until you log out. We do not use analytics or advertising trackers.

How we use it

• To formalize your project and write the results back to your repository.
• To email you login links, confirmation codes, and notices about your projects, such as a completed run or a project that needs setup.
• To operate, debug and improve the pipeline. Members of the team read project content, pipeline output and logs when they investigate a run that failed or stalled.

Who else receives it

• AI model providers. The pipeline sends text from your project, and the Lean code derived from it, to large language models. Today these are models from Anthropic, OpenAI and DeepSeek. We reach them through an AI gateway operated by Cornell University and, for some steps, directly from the provider. The models we use change over time. All of the model providers we use have guaranteed that they do not use our data to train new models. Beyond that, each provider handles what it receives under its own terms, which we do not control.
• Overleaf or GitHub. We push results into the repository you connected. Anyone who has access to that repository can see them.
• Resend delivers the email we send you and receives the email you send us.
• Amazon Web Services hosts our server.
• Google Fonts serves the typeface on these pages, so your browser contacts Google when it loads them.

We do not sell your data or share it for any purpose other than processing the formalization, except for the benchmark use described below, which you have to turn on yourself.

Benchmark use

Each project has a benchmark setting, which is off unless you turn it on. If you turn it on, the project team may contact you about turning your project into a problem for the Autoformalization for the Working Mathematician benchmark. We will not publish any part of your project without your agreement. You can change the setting at any time under Edit on your dashboard.

How long we keep it

• Projects. We keep our copy of a project while it is connected. When you disconnect it, we delete its record and run history at once and set our copy aside for deletion, which happens about 30 days later. Log files from past runs may be kept longer.
• Your repository. Disconnecting does not remove mathcopilot.sty or the math_copilot/ folder from your own project. Those are yours to keep or delete.
• Your account and access request. We keep these until you ask us to delete them.
• Model providers. We cannot recall text that has already been sent to a model provider. Its retention follows that provider's terms.

Security

Connections to this site use HTTPS. We store your email addresses, your Overleaf project ID and your Overleaf Git token encrypted. Your name, your institution and our copy of your project are stored unencrypted on the server. No system is completely secure, so do not connect work that you could not afford to have disclosed.

Your choices

• Change your name and institution, and add or remove email addresses, under Manage preferences on your dashboard.
• Disconnect a project on your dashboard at any time.
• Email [email protected] to get a copy of what we hold about you, to withdraw an access request, or to delete your account.

Changes to this policy

If we change this policy we will update the date at the top of this page. If a change affects how we handle projects that are already connected, we will email you before it takes effect.