Policies

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

Confidentiality

We treat everything you send as confidential. We do not publish your paper, code or results, and we do not list your project as an example, unless you give written permission. We will sign a reasonable NDA on request.

Use of AI tools

We work with AI assistance, including commercial models from Anthropic and OpenAI, under human direction. Only the parts of your material needed for the work are sent to these providers, and only after you authorize it. Providers may retain data for a limited period under their own terms; where a provider offers it, we use settings that exclude your material from model training. No cloud service can promise absolute secrecy. If your work must not be processed by third-party AI, tell us before you send it.

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.