DISCLAIMER: This post is a pedagogical tutorial on theorem proving for hybrid-time dynamical systems and is not intended as a serious analysis of any actual disease.

During panedmics, public health professionals often suggest “social distancing”. The goal of social distancing is to slow down the spread of the disease so that public health infrastructure is not overloaded. Unfortunately, social distancing often incures a significant social and economic cost. Businesses must close, and people are isolated from their friends and family. This leads us to an interesting question: how much social distancing is enough?

Answering that question in the context of a real pandemic requires an enormous amoung of effort. In this note, we’ll consider a very simple toy model of a pandemic and use a theorem prover to derive the minimum amount of social distancing necessary to avoid hospital overload.

## SIR Models

A Susceptible-Infected-Recovered model is a simplified dynamical system model of disease spread. The basic model is a set of three ordinary differential equations:

``````s' = -b*s*i,
r' = -k*i,
i' = b*s*i - k*i
``````

where:

• `s` is the number of individuals in the population who are susceptible to the infection,
• `r` is the number of individuals in the population who are recovered (we make the assumpption that once an individual is recovered they will not get the disease again; this assumption obviously doesn’t always hold), and
• `i` is the number of currently infected individuals.

In addition to these variables, the system also has two parameters:

• `b` is the number of contacts individuals make each day, and
• `k` is the recover rate (the number of individuals who change from infected (`i`) to recovered (`r`) each day.

Our goal is to allow as much contact between inviduals as possible while keeping the infected rate (`i`) below hospital’s capacity (`capacity`). In terms of the model, we would like to know: how large we can let `b` get before `i` goes above `capcity`?

This is a reachability property of the SIR model: we would like to know, given some initial conditions on `s`, `i`, and `r`, whether the flow of the SIR differential equations will reach point where `i < hospitalCapcity`. The KeYmaera X theorem prover was designed to explore exactly these types of reachability properties.

## A Quick Introduction to Differential Dynamic Logic and KeYmaera X

In this note, we will use KeYmaera X to discover values of `b` that keep the value of `i` below `hospitalCapcity`. KeYmaera X is a theorem prover for differential dynamic logic. This logic allows you to state and prove reachability properties of differential equations by writing formulas such as:

``````init -> [{ODEs}]property
``````

where,

• `init` is a formula of first order logic over real-valued variables (e.g., `x>0 & y>0`),
• `ODEs` is a system of differential equations,
• `property` is also a formula of first order logic over real-valued variables (e.g., `i < capacity`),

and the meaning of the formula `init -> [{ODEs}]property` is: starting from a set described by the formula `init`, any flow of the different equaltions `ODEs` will stay within the set described by `property`.

For example, we can state properties such as: `x>0 & y>0 -> [{x'=y}]x>0`; i.e., if `x` starts positive and has a positive derivative then the value of `x` will remain positive throughout the flow of the equation `x'=y`.

## Finding a Safe Contact Rate using KeYmaera X

Here’s a simple SIR model written in KeYmaera X’s input language:

``````ProgramVariables
R s, r, i, s_0, r_0, i_0, b, k, capacity;
End.
Problem
(
i < capacity &
s=s_0 &
r=r_0 &
i=i_0 &
0 < k & k < 1
)
->
[
{
s' = -b*s*i,
r' = k*i,
i' = b*s*i-k*i
}
](i<capacity)
End.
``````

Notice that this formula is not true! For example, if:

``````s_0      = 1,000,000
r_0      = 0
i_0      = 999
capacity = 1000
``````

then obviously `i` will quickly exceed `capcity`. However, we can use KeYmaera X to derive necessary and sufficient conditions on the choice of `b` in terms of any concrete choice of `s_0`, `r_0`, and `i_0`.

## Conclusion

Theorem provers are useful for more than just checking the truth of things we already know. They can also help us understand the world.