Policies

Plain-language summary. Each project is governed by its signed quote and statement of work, which take precedence over this page.

Confidentiality

Everything you send is confidential. Files go to private, encrypted storage that only our team can open, and we use them for your project only. We do not publish your paper, code or results, or list your project as an example, without your written permission. We will sign a reasonable NDA on request.

Your files

We delete the files you sent within 30 days after a project closes, or sooner if you ask. If you decide not to go ahead, we delete them within 30 days of our last exchange. Delivered Lean code is yours to keep; see Delivery below.

Use of AI tools

We work with AI models from Anthropic and OpenAI under human direction. We give them only the parts of your material the work needs, with model training on your data switched off. Like any cloud service, these providers keep short-term operational logs under their published terms. If you would like your material kept away from third-party AI entirely, tell us before you send it, and we will tell you what we can offer on those terms.

Correctness never rests on an AI model. Every delivered proof is checked by the Lean kernel, and every statement is reviewed by a person.

Assessment

Every project starts with a paid assessment of fixed price and fixed time box. Its outcome is one of: proceed (with a quote), major gap, refuted, or inconclusive. The assessment fee is credited toward the project if you go ahead.

Payment

• Assessments are paid up front.
• Projects are billed by milestone, each paid on acceptance of the agreed deliverable.
• We accept card and ACH via Stripe. Universities may pay by purchase order, Net 30.
• Every payment receives a receipt. Formal invoices and a W-9 are available on request.

Errors, gaps and stopping

If the formalization reveals a substantial error or gap in the source argument, or the work reaches the cost ceiling in the statement of work, we stop and report. The report locates the problem as precisely as we can and says what remains unchecked. You pay for the work done under the current stage; prepayment for work not performed is refunded. Continuing past a ceiling always needs your written approval.

Delivery

Before final payment you see the build log and the #print axioms report for every headline theorem. On settlement you receive the complete repository. Unless the statement of work says otherwise, you may use, publish and modify the delivered code freely; general-purpose tools we developed independently remain ours to reuse. Code built on Mathlib follows Mathlib's Apache-2.0 license.

Deadlines

We commit to dates for reports and stages. We commit to a date for a finished proof only when the assessment shows the risk is low enough, and the statement of work then says what happens if we miss it.