On October 6, 2026, OpenAI published mathematical results from an internal frontier model. The openai/math repository contains 722 manuscripts organized into 372 families, with Lean formalizations for many of the results.
For engineers building AI agents, the release suggests a concrete experiment: apply its separation between proposing a result and independently checking it to the rules that update persistent memory.
For Symptomato, the target is a familiar failure: a corrected patient record arrives, an old document is uploaded again, and the current value silently goes backward. Every extracted field can be correct while the update rules fail.
What the research gives us
The published Lean artifacts make many of the proofs available for machine checking. Verification status varies across the collection, and some results still lack formalizations. The model itself remained internal at publication.
The repository also includes verification instructions using Comparator, an existing tool from Lean FRO. OpenAI's release shows how these established tools can accompany AI-generated research results.
OpenAI additionally shares reasoning summaries, attempted-problem counts, and compute estimates. That transparency suggests another practice to carry into our experiment: report the effort required to obtain a checked result.
The transferable component is the verification workflow. Our patient-memory specification and proofs would be new application work.
Apply the idea to Symptomato
Consider a synthetic sequence for one weight observation:
- Revision 1 records 72.4 kg.
- Revision 2 explicitly corrects that observation to 72.1 kg.
- Revision 1 arrives again.
The current view must retain 72.1 kg, while history retains both revisions.
Bind each accepted structured event to an organization, patient, encounter, and assertion. Store its source lineage, source-issued revision, operation, value, and immutable provenance. Compare revisions only within that lineage. Independent sources need separate reconciliation rules.
Corrections carry complete replacement values, allowing revision 2 to be accepted before revision 1. Arrival order never determines precedence.
The ledger stores distinct structured events. Equality includes stable payload and provenance; transport delivery timestamps and delivery IDs stay outside it. Reusing a version-specific event ID with different content produces an ingestion conflict, with both candidates preserved.
Derive the current view from the highest revision for each scoped assertion and source. A consistent assertion becomes active; a retraction removes its active value while preserving history. Incompatible operations or values at the highest revision become a visible conflict.
Prove the insertion layer first
The smallest layer fits into a finite-set model:
import Mathlib.Data.Finset.Insert
variable {Event : Type} [DecidableEq Event]
def ingest (s : Finset Event) (e : Event) : Finset Event :=
insert e s
theorem retry_is_noop (s : Finset Event) (e : Event) :
ingest (ingest s e) e = ingest s e :=
Finset.insert_idem e s
theorem delivery_order_independent
(s : Finset Event) (a b : Event) :
ingest (ingest s a) b = ingest (ingest s b) a :=
Finset.insert_comm b a s
theorem accepted_event_is_retained
(s : Finset Event) (e : Event) :
e ∈ ingest s e :=
Finset.mem_insert_self e s
These statements reuse existing Mathlib finite-set laws. The model covers evidence insertion only. Event validation and the current-record projection still need their own definitions and proofs.
The third obligation is essential: a function that ignores every event would also be idempotent and independent of delivery order.
Implement the projection next, with explicit obligations:
- Consistent assertions at the highest revision produce the current value and its provenance.
- A strictly older revision cannot replace the current value or resurrect a retracted assertion within its lineage.
- Incompatible highest revisions produce a conflict regardless of delivery order.
- Every displayed value has stored evidence for the exact organization, patient, encounter, and assertion.
- Previously accepted events remain in the ledger after a correction.
Reuse the independent checking approach
A reviewer freezes the schema, reducer definitions, theorem statements, imports, and build configuration. The agent fills in proof bodies, using Lean diagnostics to guide bounded retries.
Give Comparator a trusted Challenge and an agent-produced Solution. Under its documented environment assumptions, it checks statement and definition agreement, permitted axioms, and acceptance of the proofs by the Lean kernel. Changes to the contract require a separate review.
Keep a minimal repository with the reviewed model, candidate proofs, generated histories, and the CI check. Pin Lean and Mathlib versions so every proof attempt runs against the same environment.
Generate proofs during development and check them independently in CI. Patient updates call the deterministic reducer.
Measure what the research workflow adds
Generate histories containing duplicates, shuffled deliveries, corrections, retractions, conflicting revisions, and repeated IDs across organizations and patients. Seed concrete bugs: prefer the last arrival, discard correction history, or omit the organization ID.
Compare a fixed property-based test suite with the same suite plus formal proof obligations, targeting the same Lean reducer implementation. Freeze each candidate's definitions before proof search while keeping the required properties unchanged. Hold model settings and proof-search budgets constant.
Report confirmed counterexamples, proof completion, human effort, elapsed time, and model cost. A timeout means the search failed to produce a proof; it does not establish a bug.
Define the production boundary
The guarantees apply to the formal model. A separately written Python reducer needs a correspondence argument; differential tests provide evidence, not a formal equivalence proof. Calling an implementation compiled from checked Lean definitions reduces that gap. Parsing and database integration still need validation.
Stored provenance also does not establish that an LLM interpreted the source correctly or extracted every relevant fact.
OpenAI's math release makes this a concrete engineering experiment: study the published proof artifacts and checking workflow, specify one memory operation, and measure the value of independently checked proofs. For Symptomato, that first operation is updating a fact without letting a stale document undo its correction.
Top comments (7)
The theorem retry_is_noop holds for the same event arriving twice, and by your equality rule two events are the same only when payload and provenance match. The motivating case is an old document uploaded again, and unless the file itself is deduplicated first, an upload goes back through extraction. If the second pass differs from the first in anything that counts toward equality, a unit or a rounding is enough, insert keeps both events and the theorem says nothing about the case that motivated it. Your rule for a reused version-specific event ID with different content turns that into an ingestion conflict, but only if the ID comes from the source revision and not from the extraction pass, and then a re-upload meant to be a no-op becomes a conflict on a revision that is already superseded.
For a re-upload the guarantee moves to the projection, to the rule that a strictly older revision cannot replace the current value, and that rule holds only if the extractor reads the source-issued revision off the document correctly each time. The question about ordering by source revision carries the whole guarantee for this case. A document with no revision number of its own, a scan or a letter, needs its own definition in the model before the projection proof says anything about it.
A cheap number before the proof work: extract the same documents twice and count how often the two events are equal under your equality. That share is how often retry_is_noop covers a re-upload at all, and the remainder is the share that rests on the revision being read right.
Thanks, this points out a gap in how I framed the example.
retry_is_noopproves idempotence only when the exact same event is inserted twice. It does not prove that uploading the same document again is a no-op after extraction. If a second extraction produces a different payload, both events are retained; and reusing a source-revision ID with different content needs its own handling.I should also distinguish that ingestion-level inconsistency from a conflict in the current view. A discrepancy on an already superseded revision should remain visible in the history, but it must not displace or block the value from a higher revision. The projection guarantee depends on correctly reading the source-issued revision each time. For documents without a reliable revision of their own, the model needs an explicit identity and ordering policy first.
Your proposed measurement is a useful first step: re-extract the same documents and measure how often the resulting events are equal under the defined identity rule. That tells us how often exact-event idempotence covers a re-upload, while leaving the revision-reading assumption as a separate obligation.
The weight example (72.4 → corrected 72.1 → revision 1 arrives again) is a great test case, because every extracted field is right and the system still goes backwards. That's the kind of bug that unit tests on the extractor never catch.
The separation between proposing and independently checking is the transferable part, agreed. Before full Lean proofs, though, I'd try a property-based test as a cheaper first step: generate random sequences of revisions, corrections and replays, apply them in random orders, and assert that the current view equals what the latest explicit revision says. It finds the counterexamples quickly, and the properties become the spec you'd later formalize.
How are you ordering revisions: by the source-issued revision number, or by arrival time? Replays are only safe if it's the former and every source issues them reliably.
Agreed. Property-based tests are a good first step: generate revision histories, replay and shuffle deliveries, then check that the current view is determined by the highest explicit revision. That also gives us concrete counterexamples before investing in proofs.
I’d order revisions by the source-issued revision number within a specific assertion lineage, never by arrival time. That depends on the source issuing reliable, monotonic revisions. If it doesn’t, we shouldn’t infer precedence from delivery order; we’d need to surface the ambiguity or define a separate reconciliation rule.
For the same lineage and highest revision, do you represent incompatible values as one conflict object or retain both candidate events and derive the conflict from them?
I’d retain both candidate events in the immutable ledger and derive the conflict in the current view. That keeps the evidence intact and makes the conflict reproducible: same lineage, same highest revision, incompatible values or operations. The view can point to both events; a later revision or an explicit reconciliation rule can resolve it.
Some comments may only be visible to logged-in visitors. Sign in to view all comments. Some comments have been hidden by the post's author - find out more