Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Classwise permanence for weakly reversible mass-action systems

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves the permanence conjecture for every finite weakly reversible mass-action system with fixed positive rate constants. Every positive stoichiometric compatibility class, even an unbounded one, has a common compact convex forward-invariant absorbing set. All positive trajectories in that class therefore eventually share positive lower and finite upper concentration bounds. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments

What the papers state

Theorem 1.1

In Uniform Permanence in Weakly Reversible Mass-Action Systems, 5 October 2026

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

Let C\subset\Z_{\geq0}^d be finite, let R\subset C\times C be weakly reversible, and fix positive rate constants in (1.1). For every positive stoichiometric class P there is a nonempty compact convex set K_P\subset P with the following properties. Every initial point x^0\in P gives a unique global positive solution, and there is a finite T(x^0)\geq0 such that

x(t)\in K_P\qquad(t\geq T(x^0)).

Moreover, K_P is forward invariant. In particular, there is \eps_P\in(0,1), depending only on the network, the fixed rates, and P, such that every such solution satisfies

\eps_P\leq x_i(t)\leq\eps_P^{-1} \qquad(1\leq i\leq d,\ t\geq T(x^0)).

No Lean statement in the release is paired with this theorem.

Theorem 1.1

In Boundedness and persistence of weakly reversible mass-action systems

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

Let d\ge1, let \mathcal C\subset\mathbb Z_{\ge0}^d be finite, let \mathcal R be weakly reversible, and let all reaction rates be positive constants. For every x^0\in\R_{>0}^d, the solution of (1.1) with x(0)=x^0 exists for every t\ge0. There is a number \varepsilon\in(0,1), depending on the network, the rates, and x^0, such that

\varepsilon\le x_i(t)\le\varepsilon^{-1} \qquad(t\ge0,\ 1\le i\le d).

The release does not say which paper theorem its catalogue describes. Both statements above are shown whole, the closer match to the description’s wording first. The atlas has not reviewed either choice.

Reported proof verification
One Lean statement in the release; two independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Two current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Uniform Permanence in Weakly Reversible Mass-Action Systems

5 October 2026, current edition.

Read it herePDF

We prove the permanence conjecture for finite weakly reversible mass-action systems with fixed positive reaction rates. Every positive stoichiometric compatibility class admits one compact convex forward-invariant set that every positive trajectory in that class enters in finite time, even when the class is unbounded. The set depends only on the network, the rates, and the class; the entry time may depend on the initial state. Thus, after its entry time, every concentration satisfies the same positive lower and finite upper bounds throughout that class.

Boundedness and persistence of weakly reversible mass-action systems

Undated, current edition.

Read it herePDF

We prove the boundedness and persistence conjectures for finite weakly reversible mass-action systems with positive constant reaction rates. For every positive initial condition, the solution exists for all forward time, and every concentration remains bounded above and bounded away from zero. The bounds may depend on the initial condition, and no boundedness assumption is imposed on its stoichiometric compatibility class.

One Lean statement in this family

Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

MassAction

The paper states

Theorem 1.1

In Boundedness and persistence of weakly reversible mass-action systems

Let d\ge1, let \mathcal C\subset\mathbb Z_{\ge0}^d be finite, let \mathcal R be weakly reversible, and let all reaction rates be positive constants. For every x^0\in\R_{>0}^d, the solution of (1.1) with x(0)=x^0 exists for every t\ge0. There is a number \varepsilon\in(0,1), depending on the network, the rates, and x^0, such that

\varepsilon\le x_i(t)\le\varepsilon^{-1} \qquad(t\ge0,\ 1\le i\le d).

The words they share: reaction, integer, solution, network, action, mass, reversible, weakly, positive, varepsilon, depending, rates, finite, constants.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Global boundedness and persistence for weakly reversible mass-action systems

MassAction.lean, the release lists it as a supporting statement.

theorem global_bounded_persistent_solution :    ∀ (d : ℕ) (N : ReactionNetwork d) (κ : Reaction N → ℝ),      0 < d → WeaklyReversible N → (∀ e, 0 < κ e) →      ∀ x0 : Fin d → ℝ, PositiveState x0 →      ∃ ε : ℝ, 0 < ε ∧ ε < 1 ∧        (∃ x : ℝ → (Fin d → ℝ), IsGlobalForwardSolution N κ x0 x) ∧        ∀ x : ℝ → (Fin d → ℝ), IsGlobalForwardSolution N κ x0 x →        ∀ t : ℝ, 0 ≤ t → ∀ i : Fin d, ε ≤ x t i ∧ x t i ≤ ε⁻¹ := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express a weaker statement than the advertised result (their term: “weaker-statement”).

Their note: Lean gives, for each positive initial state x0, an ε = ε(N, κ, x0) with ε ≤ x_i(t) ≤ 1/ε for all t ≥ 0 (boundedness and persistence of each trajectory). The summary’s permanence (a common compact convex forward-invariant absorbing set for every positive stoichiometric class, uniform over its trajectories) is not stated; docs admit ‘the bound may depend on... the initial state’.

Definitions the group asks readers to compare with the paper: IsGlobalForwardSolution N κ x0 x := x 0 = x0 ∧ ∀ t ≥ 0, HasDerivAt x (massAction N κ (x t)) t (two-sided derivative at t = 0, harmless for forward solutions of a polynomial field)

“weaker-statement”, in their words: The challenge statements do not imply the headline claim: they state a nontrivially weaker statement.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).

The gap they name: The headline claims classwise permanence (October 5 manuscript ‘Uniform Permanence in Weakly Reversible Mass-Action Systems’); the Comparator statement gives only boundedness and persistence with initial-state-dependent ε (September 25 manuscript). The scope note states the initial-state dependence but never says permanence is omitted.

“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The boundedness and persistence conjectures for mass-action systems ask whether positive concentrations remain finite and separated from zero. The formalization proves this for every finite weakly reversible reaction network with positive constant reaction rates and every strictly positive initial state. A global forward solution exists, and one $\varepsilon\in(0,1)$ bounds every concentration of every global forward solution between $\varepsilon$ and $\varepsilon^{-1}$ for all nonnegative times. The bound may depend on the network, rates, and initial state.

AI-drafted comparisons, with no recorded human review

  • Global boundedness and persistence for weakly reversible mass-action systems MassAction

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: global boundedness and persistence for every weakly reversible mass-action network with positive constant rates, with bounds depending on the network, rates and initial state. The uniform permanence of the family’s later paper is not part of it.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Global boundedness and persistence for weakly reversible mass-action systems MassAction

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

Follow-up work by others

  • Palomar Registry, Palomar registry listing (api/v1/results), read 2026-10-11, 11 October 2026. Source

    PALOMAR-2026-10-09-000015 (Michael Mislan) adapts the release’s mass-action barrier library for endotactic permanence.

  • Palomar Registry, Palomar registry listing (api/v1/results), read 2026-10-11, 11 October 2026. Source

    PALOMAR-2026-10-11-000011 (Michael Mislan) builds on the same release mass-action library for shared-resource systems.

  • Michael Mislan, Uniform permanence of endotactic reaction networks with measurable rates (PALOMAR-2026-10-09-000015), 9 October 2026. Source

    Registered 2026-10-09T19:55:24Z; relationship to the release recorded as adapts.

References outside the release

Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 149 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 149 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form