Dynamical systems and ergodic theory · Result 149

Classwise permanence for weakly reversible mass-action systems

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Uniform Permanence in Weakly Reversible Mass-Action Systems

OpenAI · October 5, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Uniform-Permanence-in-Weakly-Reversible-Mass-Action-Systems-October-5-2026,
  author = {{OpenAI}},
  title = {{Uniform Permanence in Weakly Reversible Mass-Action Systems}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Uniform-Permanence-in-Weakly-Reversible-Mass-Action-Systems-October-5-2026/permanence.pdf}{OAI:Uniform-Permanence-in-Weakly-Reversible-Mass-Action-Systems-October-5-2026}},
  year = {2026}
}

Boundedness and persistence of weakly reversible mass-action systems

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026,
  author = {{OpenAI}},
  title = {{Boundedness and persistence of weakly reversible mass-action systems}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026/paper.pdf}{OAI:Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Boundedness and persistence of weakly reversible mass-action systems

Scope

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.

Comparator links

Result	Comparator statement
Global boundedness and persistence for weakly reversible mass-action systems	MassAction.lean

Scope note on GitHub →