Re: [isabelle] A proof assistant approach to the COVID-19 public health crisis

[ Continuation of: ]

> Am 26.03.2020 um 13:47 schrieb Makarius <makarius at>:
> On 26/03/2020 12:47, Jose Manuel Rodriguez Caballero wrote:
>>  In your post, you expressed that your priority is to stop the increase in the number of infections. Although this is important, it will not stop the exponential growth of the pandemic.
> Note that exponential growth does not exist in nature. In the real world it is
> mainly restricted to the imagination of economists.
> The standard model for spreading biological viruses (as well as rumors or
> gossip) is the Logistic Function (or Sigmoid): it looks exponential initially,
> has a turning point, and converges to a constant value. E.g. see the teaching
> material

I find this argument very dangerous, as it amounts to denying the basically exponential character of the pandemic.

Also the article you refer to seems to argue with limited resources only, which in this case is the number of susceptible persons.
If we follow the estimation used by Bach at
for "herd immunity (at 40% to 70%)," and a fatality rate "between 0.6% in South Korea and 4.4% in Iran" mentioned by Pueyo at
(mainly depending on whether a hospital overload will occur), then the overall share will be
between 0.24% (= 40%*0.6%) and 3.08% (= 70%*4.4%) of the population that will die if exponential growth isn't stopped.
Since hospital overload can be assumed, rather the latter number is likely to apply.

"Two fundamental strategies are possible: (a) mitigation, which focuses on slowing but not necessarily stopping epidemic spread – reducing peak healthcare demand while protecting those most at risk of severe disease from infection, and (b) suppression, which aims to reverse epidemic growth, reducing case numbers to low levels and maintaining that situation indefinitely. [...] However, the resulting mitigated epidemic would still likely result in hundreds of thousands of deaths and health systems (most notably intensive care units) being overwhelmed many times over. For countries able to achieve it, this leaves suppression as the preferred policy option."

"Going for 'herd immunity' at this point does not seem a viable option, as this will put NHS at an even stronger level of stress, risking many more lives than necessary.
By putting in place social distancing measures now, the growth can be slowed down dramatically, and thousands of lives can be spared. We consider the social distancing measures taken as of today as insufficient, and we believe that additional and more restrictive measures should be taken immediately, as it is already happening in other countries across the world."

One can use more sophisticated models such as the SEIR model used in,
but clearly exponential growth comes nearer to reality than linear growth.

> A very important parameter in this model is the number of unknown/unmeasured
> infections: after all Covid-19 has only mild health consequences and goes very
> often undetected. This hidden parameter restricts the ultimate limit of the
> logistic function (among other side-conditions and assumptions).
> Note that for Germany, I presently see less than linear growth of reported
> measurements at
> The authorities behind that are a bit slow in handing data to the central
> entity --- the Robert Koch Institute in Berlin. So it often takes a few days
> for the values for each day to stabilize. (Other sources claim to have better
> data in real-time, but I don't follow that.)

The pandemic by nature has exponential growth, as each infected person on average infects a certain number of other persons.
Data may be insufficient and/or some advances may have been achieved in lowering the effective reproductive number, so on the surface the graph shortly might look linear.

But without lowering the effective reproductive number to 1.0 or less, exponential growth can't be stopped.
With an effective reproductive number above 1.0, the curve cannot be "flattened", but only stretched, which doesn't affect the exponential character at all.
To compare the ratio k between two different exponential bases x and y, assume:   x^n = y^(k*n)
This yields:   k = log_y(x)
or:   k = log_10(x)/log_10(y)
For example:   log(1.33)/log(1.1) = 2.9921141983 = (approx.) 3
In other words, lowering the daily factor or the effective reproductive number from 33% to 10% will stretch the curve by factor 3 (e.g., hospital overload in 30 instead of 10 days).
For the current values, see:
Unfortunately, my estimation proved correct, and with 63.4 % at the linear translation the day before yesterday France faced the same hospital overload as Italy with this value.
I would love to be proved wrong about this, but as Germany has passed this threshold, too, and with about four times as much intensive care beds than Italy, and a current doubling period of 5.62 days, Germany might face the same situation in 10 or 14 days.

For Germany, the actual link is:

More links are provided at:


Ken Kubota

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.