What Agent Builders Can Borrow from OpenAI's Math Research

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.