pith. machine review for the scientific record. sign in

arxiv: 2605.02474 · v1 · submitted 2026-05-04 · 💻 cs.LO

Recognition: 3 theorem links

· Lean Theorem

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL

David B. Hulak , Arthur F. Ramos , Ruy J. G. B. de Queiroz
Authors on Pith no claims yet

Pith reviewed 2026-05-08 18:14 UTC · model grok-4.3

classification 💻 cs.LO
keywords Isabelle/HOLSIR epidemic ODEformal verificationPicard-Lindelof theoremqualitative analysisreusable lemmasArchive of Formal Proofsglobal existence
0
0 comments X

The pith

Isabelle/HOL proofs transfer local Picard-Lindelof flows to a unique global forward SIR solution with conservation, invariance, and threshold conditions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper builds reusable lemmas in Isabelle/HOL that link the Archive of Formal Proofs local-flow construction to classical qualitative properties of the mass-action SIR epidemic model. It first verifies sign, conservation, and monotonicity facts on local flow segments, then uses compactness of the nonnegative simplex to extend those segments to a unique global forward flow on every interval [0,b] with b>0. The results therefore hold for the concrete constructed solution rather than for an arbitrary assumed trajectory. The work supplies homogeneous-linear scalar lemmas for compartment equations of the form X'(t)=f(t)X(t), derivative-sign rules, three-compartment conservation, and a transfer bridge to the AFP infrastructure, while leaving stability and asymptotic questions unformalized.

Core claim

The central claim is that the local AFP flow segments for the SIR vector field satisfy the classical Kermack-McKendrick phase-plane relation, nonnegative orthant invariance, total-population conservation, infectious-compartment monotonicity governed by the basic reproduction ratio, and compartment bounds; these facts lift to the unique global forward flow on [0,b] for arbitrary b>0 because the nonnegative simplex is compact and forward-invariant.

What carries the argument

The reusable layer of homogeneous-linear scalar compartment lemmas for equations X'(t)=f(t)X(t) together with the AFP Picard-Lindelof local-flow construction and the nonnegative simplex as compactness witness.

If this is right

  • The SIR model admits a unique global forward solution on every interval [0,b] with b>0.
  • The nonnegative orthant is forward-invariant under the SIR flow.
  • Total population is exactly conserved for all forward time.
  • Infectious-compartment growth or decay is governed by whether the initial susceptible fraction exceeds the threshold ratio.
  • The classical Kermack-McKendrick conserved quantity holds along every trajectory of the constructed solution.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The scalar lemmas for X'(t)=f(t)X(t) and derivative-sign monotonicity can be instantiated for other three-compartment mass-action systems such as SEIR without repeating the AFP bridge.
  • Because the proofs apply to the concrete AFP-constructed flow rather than to an arbitrary solution, they can serve as a verified kernel for further certified statements about finite-time bounds or threshold phenomena.
  • The separation between reusable scalar infrastructure and the specific SIR transfer bridge makes it feasible to replace the SIR vector field with a nearby model while preserving the qualitative lemmas.

Load-bearing premise

The SIR vector field must satisfy the local Lipschitz condition so that the AFP Picard-Lindelof infrastructure produces unique local flow segments that can be extended globally using compactness of the nonnegative simplex.

What would settle it

An explicit counterexample, inside the Isabelle artifact, in which either total population is not conserved, the nonnegative orthant is left by some trajectory, or the Kermack-McKendrick relation fails to hold along the constructed global forward flow on [0,b].

Figures

Figures reproduced from arXiv: 2605.02474 by Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz.

Figure 1
Figure 1. Figure 1: Closed-population SIR compartment flow. The transmission term moves individuals view at source ↗
Figure 2
Figure 2. Figure 2: Proof order for avoiding circularity. Arrows denote proof dependency: sign facts are view at source ↗
Figure 3
Figure 3. Figure 3: Illustrative schematic phase-plane sketch, drawn as a level-curve diagram rather than view at source ↗
read the original abstract

We present a mechanically checked Isabelle/HOL bridge from the Picard-Lindelof flow infrastructure in the Archive of Formal Proofs (AFP) to selected qualitative facts for the mass-action, closed-population SIR epidemic ODE. The epidemiological facts are classical; the contribution is reusable theorem infrastructure connecting the AFP local-flow construction to global forward existence, uniqueness, forward invariance of the nonnegative orthant, conservation, monotonicity, the Kermack-McKendrick conserved phase-plane relation, compartment bounds, and threshold-ratio conditions for infectious growth and monotonicity. The proof first establishes sign and conservation facts for local AFP flow segments, then uses the conserved nonnegative simplex as the compactness witness for extending the flow to all forward times. The finite-interval qualitative facts are then transferred to the unique AFP forward flow on arbitrary intervals [0,b] with b>0, so the results apply to the constructed Isabelle/AFP SIR solution rather than to an assumed trajectory. The reusable layer provides homogeneous-linear scalar compartment lemmas for equations X'(t)=f(t)X(t), derivative-sign monotonicity, three-compartment conservation, and an SIR transfer bridge to the AFP flow infrastructure. We do not formalize stability, final-size, or asymptotic theory. The accompanying Isabelle artifact builds with Isabelle 2024 and AFP 2024 and contains no sorry or oops proof placeholders.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper presents a mechanically checked Isabelle/HOL formalization bridging the AFP Picard-Lindelöf local-flow infrastructure to global forward existence, uniqueness, and selected qualitative properties of the closed-population mass-action SIR ODE. It proves forward invariance of the nonnegative simplex, conservation, monotonicity, the Kermack-McKendrick phase-plane relation, compartment bounds, and threshold conditions for infectious growth, then transfers these facts to the unique global forward flow on arbitrary intervals [0,b]. A reusable layer of homogeneous-linear scalar lemmas for equations of the form X'(t)=f(t)X(t), derivative-sign monotonicity, and three-compartment conservation is provided, with all steps verified without placeholders.

Significance. The work supplies certified, reusable theorem infrastructure that applies directly to the constructed AFP global SIR flow rather than to an assumed trajectory. Strengths include the mechanically checked proofs, the parameter-free reusable scalar lemmas independent of SIR nonlinearity, the compactness argument for global extension, and the clean build on Isabelle 2024/AFP 2024. This strengthens formal methods support for classical qualitative results in mathematical epidemiology.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for the positive assessment. We appreciate the recommendation to accept and are pleased that the reusable theorem infrastructure, the bridge from AFP local flows to global SIR solutions, and the parameter-free scalar lemmas were highlighted as strengths.

Circularity Check

0 steps flagged

No significant circularity; derivation is mechanically verified against external AFP infrastructure

full rationale

The paper's derivation chain consists of formal Isabelle/HOL proofs that transfer sign, conservation, monotonicity, and Kermack-McKendrick facts from local AFP Picard-Lindelöf flow segments to a unique global forward flow on the nonnegative simplex. All steps are machine-checked with no placeholders. The reusable scalar lemmas apply to homogeneous-linear equations X'(t)=f(t)X(t) and are independent of the SIR nonlinearity. The central results rest on the external AFP library and standard ODE theory (local Lipschitz condition, compactness of the invariant simplex) rather than any self-definition, fitted parameter renamed as prediction, or load-bearing self-citation. No quantity is defined in terms of itself, and the artifact builds cleanly under stated Isabelle/AFP versions.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the AFP local-flow construction and standard assumptions about the SIR vector field; no free parameters or new entities are introduced.

axioms (2)
  • standard math Picard-Lindelof theorem for local existence and uniqueness of flows (AFP library)
    Provides the base local-flow segments that are later extended to global time.
  • domain assumption The SIR right-hand side is locally Lipschitz continuous
    Required for the AFP infrastructure to apply to the specific SIR vector field.

pith-pipeline@v0.9.0 · 5558 in / 1309 out tokens · 59116 ms · 2026-05-08T18:14:49.714693+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 28 canonical work pages

  1. [1]

    R. M. Anderson and R. M. May.Infectious Diseases of Humans: Dynamics and Control. Oxford University Press, 1991. doi:10.1093/oso/9780198545996.001.0001

    work page doi:10.1093/oso/9780198545996.001.0001 1991

  2. [2]

    Ballarin

    C. Ballarin. Locales: A module system for mathematical theories.Journal of Automated Reasoning, 52(2):123–153, 2014. doi:10.1007/s10817-013-9284-7

    work page doi:10.1007/s10817-013-9284-7 2014

  3. [3]

    Boldo, C

    S. Boldo, C. Lelay, and G. Melquiond. Coquelicot: A user-friendly library of real analysis for Coq.Mathematics in Computer Science, 9(1):41–62, 2015. doi:10.1007/s11786-014-0181-1

    work page doi:10.1007/s11786-014-0181-1 2015

  4. [4]

    Brauer and C

    F. Brauer and C. Castillo-Chávez.Mathematical Models in Population Biology and Epi- demiology, volume 40 ofTexts in Applied Mathematics. Springer, 2nd edition, 2012. doi:10.1007/978-1-4614-1686-9

    work page doi:10.1007/978-1-4614-1686-9 2012

  5. [5]

    Brauer, C

    F. Brauer, C. Castillo-Chávez, and Z. Feng.Mathematical Models in Epidemiology, vol- ume 69 ofTexts in Applied Mathematics. Springer, 2019. doi:10.1007/978-1-4939-9828-9. 30

    work page doi:10.1007/978-1-4939-9828-9 2019

  6. [6]

    Ciocchetta and J

    F. Ciocchetta and J. Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems.Theoretical Computer Science, 410(33–34):3065–3084, 2009. doi:10.101 6/j.tcs.2009.02.037

    2009

  7. [7]

    Diekmann, H

    O. Diekmann, H. Heesterbeek, and T. Britton.Mathematical Tools for Understanding Infectious Disease Dynamics. Princeton Series in Theoretical and Computational Biology. Princeton University Press, 2013

    2013

  8. [8]

    Diekmann and J

    O. Diekmann and J. A. P. Heesterbeek.Mathematical Epidemiology of Infectious Diseases: Model Building, Analysis and Interpretation. Wiley, 2000

    2000

  9. [9]

    Diekmann, J

    O. Diekmann, J. A. P. Heesterbeek, and J. A. J. Metz. On the definition and the compu- tation of the basic reproduction ratioR0 in models for infectious diseases in heterogeneous populations.Journal of Mathematical Biology, 28(4):365–382, 1990. doi:10.1007/BF0017 8324

    work page doi:10.1007/bf0017 1990

  10. [10]

    and Heesterbeek, J

    O. Diekmann, J.A. P. Heesterbeek, and M. G.Roberts. Theconstruction of next-generation matrices for compartmental epidemic models.Journal of the Royal Society Interface, 7(47):873–885, 2010. doi:10.1098/rsif.2009.0386

    work page doi:10.1098/rsif.2009.0386 2010

  11. [11]

    Fisher and T

    J. Fisher and T. A. Henzinger. Executable cell biology.Nature Biotechnology, 25(11):1239– 1249, 2007. doi:10.1038/nbt1356

    work page doi:10.1038/nbt1356 2007

  12. [12]

    N. Fulton. Analyzing disease spread models using a theorem prover. Web note, 2020. https://nfulton.org/2020/03/27/SIR-Models-In-KeYmaeraX/, last checked 3 May 2026

    2020

  13. [13]

    KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

    N. Fulton, S. Mitsch, J.-D. Quesel, M. Völp, and A. Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. InAutomated Deduction – CADE-25, volume 9195 ofLNCS, pages 527–538. Springer, 2015. doi:10.1007/978-3-319-21401-6_36

    work page doi:10.1007/978-3-319-21401-6_36 2015

  14. [14]

    Harrison,The HOL Light theory of Euclidean space, Journal of Automated Reasoning, 50(2):173–190, 2013.doi: 10.1007/s10817-012-9250-9

    J. Harrison. The HOL Light theory of euclidean space.Journal of Automated Reasoning, 50(2):173–190, 2013. doi:10.1007/s10817-012-9250-9

    work page doi:10.1007/s10817-012-9250-9 2013

  15. [15]

    H. W. Hethcote. Qualitative analyses of communicable disease models.Mathematical Biosciences, 28(3–4):335–356, 1976. doi:10.1016/0025-5564(76)90132-2

    work page doi:10.1016/0025-5564(76)90132-2 1976

  16. [16]

    H. W. Hethcote. The mathematics of infectious diseases.SIAM Review, 42(4):599–653,

  17. [17]

    doi:10.1137/S0036144500371907

    work page doi:10.1137/s0036144500371907

  18. [18]

    J. Hölzl. Markov models.Archive of Formal Proofs, 2012. Archive of Formal Proofs entry, https://www.isa-afp.org/entries/Markov_Models.html

    2012

  19. [19]

    Hölzl, F

    J. Hölzl, F. Immler, and B. Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. InInteractive Theorem Proving (ITP 2013), volume 7998 ofLNCS, pages 279–294. Springer, 2013. doi:10.1007/978-3-642-39634-2_21

    work page doi:10.1007/978-3-642-39634-2_21 2013

  20. [20]

    F. Immler. Verified reachability analysis of continuous systems. InTools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 ofLNCS, pages 37–51. Springer, 2015. doi:10.1007/978-3-662-46681-0_3

    work page doi:10.1007/978-3-662-46681-0_3 2015

  21. [21]

    F. Immler. A verified ODE solver and the Lorenz attractor.Journal of Automated Reason- ing, 61(1–4):73–111, 2018. doi:10.1007/s10817-017-9448-y

    work page doi:10.1007/s10817-017-9448-y 2018

  22. [22]

    Immler and J

    F. Immler and J. Hölzl. Numerical analysis of ordinary differential equations in Is- abelle/HOL. InInteractive Theorem Proving (ITP 2012), volume 7406 ofLNCS, pages 377–392. Springer, 2012. doi:10.1007/978-3-642-32347-8_26. 31

    work page doi:10.1007/978-3-642-32347-8_26 2012

  23. [23]

    Immler and J

    F. Immler and J. Hölzl. Ordinary differential equations.Archive of Formal Proofs, 2012. Archive of Formal Proofs entry, https://www.isa-afp.org/entries/Ordinary_Differential_ Equations.html

    2012

  24. [24]

    ThePoincaré-BendixsontheoreminIsabelle/HOL

    F.ImmlerandY.K.Tan. ThePoincaré-BendixsontheoreminIsabelle/HOL. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 338–352. ACM, 2020. doi:10.1145/3372885.3373833

    work page doi:10.1145/3372885.3373833 2020

  25. [25]

    W. O. Kermack and A. G. McKendrick. A contribution to the mathematical theory of epidemics.Proceedings of the Royal Society A, 115(772):700–721, 1927. doi:10.1098/rspa.1 927.0118

    work page doi:10.1098/rspa.1 1927

  26. [26]

    M. Maggesi. A formalization of metric spaces in HOL Light.Journal of Automated Rea- soning, 60(2):237–254, 2018. doi:10.1007/s10817-017-9412-x

    work page doi:10.1007/s10817-017-9412-x 2018

  27. [27]

    Makarov and B

    E. Makarov and B. Spitters. The Picard algorithm for ordinary differential equations in Coq. InInteractive Theorem Proving (ITP 2013), volume 7998 ofLNCS, pages 463–468. Springer, 2013. doi:10.1007/978-3-642-39634-2_34

    work page doi:10.1007/978-3-642-39634-2_34 2013

  28. [28]

    J. D. Murray.Mathematical Biology I: An Introduction, volume 17 ofInterdisciplinary Applied Mathematics. Springer, 3rd edition, 2002. doi:10.1007/b98868

    work page doi:10.1007/b98868 2002

  29. [29]

    M. Nagumo. Über die lage der integralkurven gewöhnlicher differentialgleichungen.Pro- ceedings of the Physico-Mathematical Society of Japan. 3rd Series, 24:551–559, 1942

    1942

  30. [30]

    Paulson, and Markus Wenzel

    T. Nipkow, L. C. Paulson, and M. Wenzel.Isabelle/HOL: A Proof Assistant for Higher- Order Logic, volume 2283 ofLNCS. Springer, 2002. doi:10.1007/3-540-45949-9

    work page doi:10.1007/3-540-45949-9 2002

  31. [31]

    Park and H

    S. Park and H. Thies. A Coq formalization of Taylor models and power series for solv- ing ordinary differential equations. In15th International Conference on Interactive The- orem Proving (ITP 2024), volume 309 ofLeibniz International Proceedings in Informat- ics (LIPIcs), pages 30:1–30:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4...

    work page doi:10.4230/lipics.itp.2024.30 2024

  32. [32]

    A. Platzer. Differential dynamic logic for hybrid systems.Journal of Automated Reasoning, 41(2):143–189, 2008. doi:10.1007/s10817-008-9103-8

    work page doi:10.1007/s10817-008-9103-8 2008

  33. [33]

    Ilyes Batatia, David Peter Kovacs, Gregor N

    A. Platzer.Logical Foundations of Cyber-Physical Systems. Springer, 2018. doi:10.1007/97 8-3-319-63588-0

    work page doi:10.1007/97 2018

  34. [34]

    Y. K. Tan and A. Platzer. An axiomatic approach to existence and liveness for differential equations.Formal Aspects of Computing, 33(4):461–518, 2021. doi:10.1007/s00165-020-0 0525-0

    work page doi:10.1007/s00165-020-0 2021

  35. [35]

    Teschl.Ordinary Differential Equations and Dynamical Systems, volume 140 ofGraduate Studies in Mathematics

    G. Teschl.Ordinary Differential Equations and Dynamical Systems, volume 140 ofGraduate Studies in Mathematics. American Mathematical Society, 2012

    2012

  36. [36]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 367–381. ACM, 2020. doi:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  37. [37]

    and Watmough, James , year=

    P. van den Driessche and J. Watmough. Reproduction numbers and sub-threshold endemic equilibria for compartmental models of disease transmission.Mathematical Biosciences, 180:29–48, 2002. doi:10.1016/S0025-5564(02)00108-6

    work page doi:10.1016/s0025-5564(02)00108-6 2002

  38. [38]

    Wenzel.Isabelle/Isar—a Versatile Environment for Human-Readable Formal Proof Documents

    M. Wenzel.Isabelle/Isar—a Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Technische Universität München, 2002. https://isabelle.in.tu m.de/Isar/isar-thesis-Isabelle2002.pdf. 32

    2002