AI-generated research needs a release contract, not just a proof

A correct proof can still be an irresponsible release

AI can now produce research-shaped objects faster than communities can absorb them: theorem statements, proof sketches, formal certificates, experimental plans, code, manuscripts, and claims of novelty. The bottleneck is moving. It is no longer only whether a model can produce a plausible result. It is whether a lab can make that result inspectable, attributable, understandable, correctable, and useful without overwhelming the people who must turn output into science.

The September 29 recommendations from the independent Advisory Group on Mathematics and AI make this tension concrete. The group distinguishes papers that a responsible mathematician fully understands from results not yet understood by the people who prompted the system. For the second category, it recommends timely deposits in durable scholarly repositories, detailed system and compute disclosure, community-led development of understanding, and material support for the human work required after release. The document is advice, not a standard or legal mandate. Its value is that it treats understanding as part of the output rather than a free externality.

That matters beyond mathematics. A protein candidate, materials claim, climate finding, clinical hypothesis, or benchmark result can be internally coherent yet still fail because the training inputs were contaminated, the search missed prior work, the experimental protocol changed, the artifact cannot be reproduced, or the public description overstates what the evidence proves. The release boundary must join technical verification with research integrity.

The controversy is about throughput, incentives, and human capacity

OpenAI's August publication on ten advances in mathematics says an internal Astra model produced results across geometry, coding theory, complexity, cryptography, and other fields, with human-prepared manuscripts and Lean certificates. Its September Navier-Stokes publication added a formal proof artifact and a public account of an investigation into whether private user prompts could have influenced the result. These releases expose useful artifact patterns. They also demonstrate why a research claim cannot be reduced to a launch post and a checker result.

The opposing concern is not simply that AI proofs may contain mistakes. The Math and AI declaration argues that mathematics depends on question formation, explanation, criticism, apprenticeship, and a human transmission chain. If a proprietary system can emit many significant results while reviewer time remains fixed, publication becomes a queueing problem with scientific consequences. Priority can be disrupted before artifacts are inspectable. Researchers can lose months of work to a vague announcement. Communities can be asked to supply uncompensated verification and exposition for a company's capability demonstration.

The focused community scan supports that framing without proving consensus. The September 30 Hacker News discussion drew 118 points and 174 comments. An r/mathematics thread drew 77 points and 41 comments, while recurring r/math threads debated embargoes, credit, private-user data, formalization, and whether the release volume could exceed the field's ability to review it. Those are discussion signals, not votes on a universal policy. They identify the operational seams a release contract must expose.

A useful design therefore separates two questions. First, can the lab establish a bounded technical claim? Second, can the research community evaluate and assimilate it without depending on the lab's marketing narrative? The first question needs artifacts and verifiers. The second needs independent repositories, reviewer access, conflict handling, explanation work, and time.

Use a ten-field release contract

The contract should be created before public claims, not reconstructed after controversy. Each field has an owner, evidence, status, and blocking rule.

Do not collapse these fields into one confidence score. A result can have a verified Lean certificate and an unresolved novelty conflict. It can have strong human exposition but missing training-input provenance. It can reproduce computationally while the statistical claim remains underpowered. The release decision should preserve those differences.

Freeze the claim and its production path in a manifest

A durable repository entry should contain a machine-readable manifest next to the human paper. The goal is not to dump private reasoning traces or sensitive data. It is to identify the model-mediated transformations and exact artifacts that matter to review.

release_id: airr-2026-0042
status: external_review
claim:
  statement_sha256: "7d9c..."
  scope: "finite simple graphs under assumptions A1-A4"
  limitations: ["no weighted extension", "novelty review open in subcase C"]
generation:
  model: "lab-model-2026-09-18"
  decoding_profile: "research-search-v3"
  prompts_archive: "repo://prompts/v1"
  tools: ["literature-search@2.4", "lean@4.22", "python@3.13"]
  human_edits: "repo://editorial-diff/v1"
  elapsed_hours: 19.4
artifacts:
  manuscript: {path: "paper/v1.pdf", sha256: "a00f..."}
  formalization: {path: "lean/", commit: "21c9..."}
  experiments: {path: "runs/", manifest_sha256: "88ef..."}
verification:
  formal: "PASS"
  expert_review: "OPEN_OBJECTIONS"
  independent_reproduction: "PENDING"
credit:
  responsible_humans: ["ORCID:0000-0000-0000-0001"]
  concurrent_work_review: "IN_PROGRESS"
lifecycle:
  persistent_id: "doi:pending"
  correction_owner: "research-integrity@example.org"
  notify: ["repository", "journal", "known_downstream_citations"]

The manifest must be versioned with the artifacts. If a definition changes, the certificate is rebuilt, a reviewer objection is resolved, or a human exposition replaces a model-produced paragraph, publish a new version with an explicit diff. Never silently replace the object behind a public claim.

Prompt disclosure needs judgment. AGMAI recommends releasing prompts and a summarized chain of thought for AI-generated mathematics. A lab may also face security, privacy, intellectual-property, or model-safety constraints. The contract should record the reason for any withheld component, publish the maximum safe reproducibility detail, and let an independent reviewer inspect protected evidence under an appropriate agreement. “Proprietary” should not become a blank field.

Run verification as independent lanes, not a single gate

Research teams often use the word verification for different activities. Each catches a different failure class.

The formal lane needs its own threat model. Pin the theorem prover, compiler, dependencies, and trusted base. Build from a clean environment. Confirm that the natural-language claim maps to the encoded theorem. Check whether imported lemmas hide the substantive work. Preserve failed proof attempts when they explain scope decisions, but do not equate search exhaust with evidence.

The novelty lane should search more than titles. Record semantic search terms, theorem variants, adjacent fields, unpublished talks or preprints known to the team, and private submissions that may create conflicts. OpenAI's Navier-Stokes post is instructive because it describes an investigation into whether another researcher's private prompts influenced the result. A release process should not wait for public suspicion before it has a private-input and concurrent-work review.

Make human understanding an owned deliverable

The responsible person cannot be a ceremonial author. They should be able to restate the claim, explain the proof architecture, defend assumptions, identify weak points, answer objections, and say what remains unknown. If nobody can do that yet, label the object as an unassimilated machine-generated result rather than a normal human-authored paper.

That label does not require secrecy. A bounded preliminary release may preserve priority, reduce duplicated work, and invite specialists to test the result. It should include the artifact bundle, known limitations, verification status, conflict register, and a plan for community-led exposition. It should avoid a headline that treats unresolved review as a completed scientific fact.

Support matters because explanation and verification are expensive. AGMAI argues that labs releasing results without immediate human understanding should fund the work needed to build that understanding without directing its conclusions. A practical implementation can fund independent seminars, reading groups, formalization bounties, replication grants, open commentary infrastructure, and early-career participation. The lab publishes the funding terms and recusal rules; the community selects the questions and produces the critique.

This also protects research pipelines. If model output replaces the junior work through which researchers learn to form conjectures, debug definitions, and recognize useful failure, the field may gain answers while losing capacity. The release contract should therefore record educational artifacts: failed approaches, counterexamples, explanatory examples, prerequisite maps, and questions opened by the result. Those are not marketing extras. They are how output becomes knowledge.

Use a state machine that blocks premature certainty

def next_state(bundle):
    if not bundle.claim_is_exact or not bundle.artifact_hashes:
        return "QUARANTINED"
    if bundle.private_input_conflict or bundle.known_priority_conflict:
        return "CONFLICT_REVIEW"
    if not bundle.minimum_provenance or not bundle.correction_owner:
        return "HOLD"
    if bundle.formal_claim and not bundle.clean_formal_build:
        return "HOLD"
    if not bundle.independent_reviewer_assigned:
        return "INTERNAL_ONLY"
    if not bundle.human_understanding_ready:
        return "PRELIMINARY_UNASSIMILATED_RELEASE"
    if bundle.open_material_objections:
        return "PUBLIC_REVIEW"
    return "CANDIDATE_SCHOLARLY_RELEASE"

These states describe evidence, not prestige. “Preliminary” is not failure, and “candidate scholarly release” is not a guarantee of correctness. The state controls public wording, repository metadata, access, reviewer expectations, and what downstream systems may do with the claim.

Add event-driven transitions. A discovered prior result sends the bundle to conflict review. A failed reproduction moves it to hold. A material correction creates a new version and alerts known downstream users. A venue acceptance may change distribution but should not erase the release history. A lab retraction should leave a tombstone with reasons and artifact hashes so the scientific record remains legible.

Failure modes to rehearse before the first major release

Run a 30-day release pilot on one bounded result

1. Days 1-5: choose one result with a precise statement, appoint research, formal-methods, integrity, repository, communications, and independent-review owners, and define blocking evidence.
2. Days 4-10: freeze the production manifest, artifact hashes, human-edit diff, tool versions, compute estimate, literature search, private-input review, and known concurrent work.
3. Days 8-15: run clean formal builds or computational reruns, statement-correspondence review, adversarial cases, and an external reproduction attempt. Keep the lanes separate.
4. Days 12-20: have the responsible human produce a proof map, prerequisites, examples, limitations, open objections, and a seminar without relying on a live model to answer every challenge.
5. Days 18-24: deposit a candidate bundle in a durable repository, test identifiers and version diffs, invite comments, and rehearse a correction, priority conflict, and withdrawal.
6. Days 23-28: review public language against the exact evidence state. Publish uncertainty, unresolved objections, funding and reviewer independence, and the difference between formal and scientific validation.
7. Days 27-30: decide hold, preliminary unassimilated release, public review, or candidate scholarly release. Record the decision, dissent, next review date, and notification list.

Measure time to inspect, reproduce, explain, resolve objections, and issue a correction. Count unresolved conflicts and reviewer load. Do not optimize for papers per week. High output with low assimilation is an operational backlog, not scientific velocity.

Frequently asked questions

Does a Lean certificate make an AI-generated theorem ready to publish?

No. It can establish that an encoded statement checks under a named environment. Reviewers still need to confirm the translation, assumptions, provenance, novelty, concurrent work, human explanation, credit, and lifecycle.

Who should be listed as the author?

Follow the journal or repository policy. AI systems cannot accept responsibility. Named humans should disclose the model's contribution and claim only the work they understand, verify, and can defend. When that bar is not met, use an explicit machine-generated and not-yet-assimilated label.

Must a lab wait for complete human understanding?

Not always. A bounded preliminary release can preserve priority and enable scrutiny if artifacts are durable, limitations are prominent, the evidence state is explicit, independent work is supported, and public language does not imply settled science.

Can this contract apply outside mathematics?

Yes, with domain-specific lanes. Experimental science needs data, protocol, calibration, statistical, and replication evidence. Software and benchmarks need executable environments and contamination checks. Clinical work needs stronger ethical, regulatory, and human-subject boundaries.

What is the smallest useful implementation?

One result, one manifest, immutable artifacts, separate verification lanes, one explanation owner, one independent reviewer, one durable repository, and a tested correction path.