Isabelle/HOL proofs establish conservation, monotonicity, compartment bounds, and threshold conditions for the SIR ODE by bridging AFP local flows to global forward solutions with reusable scalar lemmas.
Harrison, The HOL Light theory of Euclidean space
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
fields
cs.LO 2years
2026 2verdicts
ACCEPT 2roles
background 1polarities
background 1representative citing papers
A machine-checked Lean 4 formalization of Stokes' theorem on smooth singular cubes with true Fréchet pullback, chain-level extensions, and comparison to prior HOL Light work.
citing papers explorer
-
Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
Isabelle/HOL proofs establish conservation, monotonicity, compartment bounds, and threshold conditions for the SIR ODE by bridging AFP local flows to global forward solutions with reusable scalar lemmas.
-
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
A machine-checked Lean 4 formalization of Stokes' theorem on smooth singular cubes with true Fréchet pullback, chain-level extensions, and comparison to prior HOL Light work.