By Aditi Viswanathan
Over the weekend, a family WhatsApp group full of mathematicians lit up over OpenAI’s latest announcement.
OpenAI reported that an internal version of Astra, its next major model, had produced 10 results that resolve or make substantial progress on long-standing problems across mathematics and theoretical computer science. Humans worked with the model to prepare the manuscripts, and the model then formalized each argument as a machine-checkable Lean certificate.
The immediate question in the group was the obvious one:
Are the proofs actually correct?
That is part of what makes the announcement so striking. Finding a proof can require enormous open-ended search, new constructions, and the coordination of ideas across multiple areas. But once the argument has been translated into a formal language such as Lean, checking whether it follows from the specified definitions and assumptions becomes a much more bounded task.
Formal verification does not settle every question. Mathematicians must still confirm that the formal statement captures the intended problem, assess the result’s novelty and significance, and understand the ideas behind the proof.
But it makes the underlying asymmetry unusually visible:
Generating the solution is hard. Checking a completed solution can be much easier.
That same asymmetry appears in a recent paper, The Future of Facts: Tracing the Factual Generation–Verification Gap. The authors call it the generation–verification gap, or GV gap: language models can often recognize a correct answer more reliably than they can produce one.
The paper focuses primarily on factual knowledge. Astra offers a vivid example in mathematical reasoning. And in regulatory medical writing, we encounter a broader, highly practical version of the same phenomenon:
It is often much easier to check a regulatory document than to author one.
A good critic is not necessarily a good author
Once a clinical study report or submission module has been drafted, we can ask a series of relatively bounded questions:
Does this number match Table 14.3.1?
Are all primary and secondary endpoints addressed?
Is this statement supported by the protocol or statistical analysis plan?
Are all required sections present?
Are terminology, abbreviations, units, and cross-references consistent?
Does the document follow the sponsor’s style guide?
Each question can become a specialized verifier. One agent checks numerical accuracy. Another checks completeness. Another validates structure. Another checks style.
These tasks are not trivial. They still require access to the correct sources, domain-specific instructions, careful engineering, and appropriate human oversight.
But they have a relatively clear shape. A number either matches its source or it does not. A required section is present or missing. An abbreviation follows the rule or it does not.
This is why quality control is such a natural application for agentic AI.
Verification decomposes
Document quality is multidimensional, but many of its dimensions can be evaluated separately.
Accuracy can be checked against source data. Compliance can be checked against regulatory requirements and sponsor templates. Consistency can be checked across terminology, abbreviations, units, and repeated values. Completeness can be checked against an inventory of required content. Clarity can be assessed against a defined rubric.
In our own work on measuring quality in regulatory medical writing, we separate quality into dimensions including accuracy, compliance, clarity, consistency, completeness, and efficiency. Each dimension requires different evidence and can be evaluated using different methods.
Because the checks are separable, the systems performing them can also be modular. A numerical-verification agent does not need to solve document structure. A style agent does not need to determine whether every efficacy endpoint was analyzed. Each verifier can be tested, measured, and improved independently.
In other words:
Verification decomposes.
That makes QC agents extremely valuable. They can reduce repetitive review work, catch issues earlier, standardize expectations, and turn an abstract idea such as “high quality” into a set of concrete, measurable requirements.
Authoring starts from the opposite direction.
Generation entangles
A QC system begins with a candidate document and asks whether it passes a collection of checks.
An authoring system must produce the candidate—and produce one that passes all of those checks simultaneously.
That changes the shape of the problem.
The system must determine which sources are relevant to each section, distinguish template instructions from study evidence, choose the appropriate level of detail, and understand where the same information must appear in different forms.
It must also reason across dependencies.
A number may be correct in isolation but inconsistent with another section. A complete description may be appropriate for the results section but too detailed for the synopsis. A conclusion may accurately summarize one table while failing to represent the totality of the evidence.
Structure affects source selection.
Source selection constrains what can be claimed.
The claims determine which tables, figures, and citations are required.
A change to one source may affect multiple sections, conclusions, cross-references, and abbreviations.
Each individual check may be relatively straightforward: Does this value match the table? Is the required heading present?
But generating a document that passes all of those checks requires solving a coupled planning and constraint-satisfaction problem across long contexts and heterogeneous sources.
The system is not merely writing sentences.
It is constructing a highly constrained artifact.
A large document is not one long prompt
This distinction has important implications for how authoring systems must be built.
A credible system cannot place every available file into a large context window and ask a model to “write the document.”
Protocols, statistical analysis plans, tables, figures, listings, templates, and style guides are fundamentally different objects. They contain different kinds of information and must be processed differently.
Before drafting begins, the system needs an intermediate representation of the document: a roadmap defining its structure, the intent of each section, the relevant sources, and the relationships among sections.
It needs hierarchical generation so that individual units can be drafted, traced, reviewed, and regenerated without treating the document as one indivisible block.
It needs persistent document state so that when a source changes, the system can identify which downstream content may have become stale.
And it needs verification throughout the workflow—not merely as a final gate, but as a feedback mechanism that helps the authoring system detect and repair its own failures.
That is the architecture we have been building at Peer: processing heterogeneous inputs, creating granular document roadmaps, mapping sources and instructions to specific subcontent, generating hierarchically, and applying style and quality checks throughout the workflow.
The goal is not “prompt in, document out.”
It is a production system for long, source-driven documents.
QC defines the target. Authoring has to reach it.
None of this diminishes the importance of QC. Strong authoring depends on strong verification.
QC agents make the quality bar explicit. They provide evaluation harnesses, regression tests, and feedback signals. They show us what failed and where the system needs to improve.
QC and authoring are therefore not competing capabilities. They are complementary layers of the same system.
But they are not equivalent in difficulty.
QC defines what good looks like. Authoring must produce it.
Or, put another way:
Build verifiers to understand correctness. Build authoring systems to satisfy correctness.
The second depends on the first—but requires substantially more.
This distinction also matters strategically.
A QC agent creates value by automating a defined check. An end-to-end authoring platform must encode much more of the underlying work: how documents are structured, how evidence becomes claims, how sections depend on one another, and how the right context should be assembled at each stage.
Every failure teaches the system something about that architecture.
An omitted endpoint may reveal the need for a stronger content model. A wrong table may expose a weakness in source mapping. An inconsistency may require explicit dependency tracking. A vague conclusion may call for better planning or an additional verification loop.
Over time, that accumulated machinery becomes meaningful intellectual property.
QC creates value by checking the work. Authoring creates a deeper moat by learning how the work fits together.
The encouraging part is that we are beginning to see the harder problem become tractable. Across customer projects, our authoring system has substantially reduced the time required to create complex regulatory documents while, in several cases, producing drafts that matched or exceeded the quality of existing manually authored work.
There is still a great deal to solve. But large-document authoring is no longer merely an aspirational use case for generative AI.
It is a difficult engineering problem that can be worked through systematically.
Correctness is not the same as understanding
The Astra announcement also points to a second distinction.
A Lean certificate can make formal correctness machine-checkable. But it does not, by itself, explain why a proof works, why the result matters, or how it changes the surrounding field.
That work still requires human understanding.
This was where the conversation among the mathematicians in my family shifted from excitement to apprehension.
If AI can produce formally valid results faster than people can absorb them, the bottleneck may no longer be proving theorems. It may be understanding their significance, integrating them into the field, and training the next generation of mathematicians to build on them.
Regulatory writing has its own version of this problem.
A document may pass a large collection of automated checks and still require an experienced medical writer, statistician, or clinician to determine whether it presents the study appropriately and communicates the right interpretation.
A value may be accurately transcribed but misleadingly emphasized.
A conclusion may be fully supported but insufficiently qualified.
A document may be complete according to a checklist while still failing to communicate the study clearly.
Verification can establish increasingly strong evidence of correctness. It cannot eliminate the need for judgment.
The future is therefore unlikely to be a simple replacement of experts by generators. It is more likely to involve a new division of work: AI systems generating and checking increasingly complex artifacts, while humans provide context, interpretation, accountability, and direction.
Verification becomes more important as generation improves
Astra demonstrates how quickly generation is advancing, even in domains defined by difficult, open-ended reasoning.
But advances in generation do not make verification less important. They make it more important.
As systems become capable of producing more complex outputs, at greater speed and scale, we need stronger mechanisms for establishing what those outputs are based on, whether they satisfy the relevant constraints, and where human judgment is still required.
In mathematics, this may mean formal certificates, independent proof checking, and expert interpretation.
In regulatory writing, it means traceable source mappings, explicit document structure, granular generation, automated QC, versioned state, and human review.
The specific mechanisms are different, but the architectural principle is the same:
Generation should not scale without verification scaling alongside it.
A builder’s version of the GV gap
Computer scientists may recognize the shape of an older question in all of this: P versus NP.
Checking a proposed solution can be much easier than finding one.
Regulatory authoring is not literally an instance of P versus NP. Neither is the process of discovering and formalizing a mathematical proof. The analogy is an engineering intuition, not a formal claim.
But after building both sides of the problem, the resemblance is hard to ignore.
Verification asks whether an artifact satisfies the constraints.
Generation must understand those constraints, resolve their interactions, and construct the artifact.
Astra shows just how far generation is beginning to advance.
It also shows why the systems surrounding generation must become better at checking, tracing, interpreting, and governing what it produces.
My takeaway remains simple:
Verification decomposes. Generation entangles.
Not a proof—just a builder’s working hypothesis:
P ≠ NP.
