COVID-19: UK predictions: now-June 2020

The logistic distribution from John Cook's excellent overview

The derivative of the logistics curve (the cumulative number of cases in an epidemic) is the logistic distribution, which looks very much like a scaled normal distribution as John Cook explains.

His graph above shows you the number of active cases as time advances: starting low, rising to an epidemic peak and then dying away. [As I write we are at -3.5σ = -5.6].

The standard deviation to use σ = 1.6 according to John Cook's article.

The Times today carries a report which allows a prediction of the course of the epidemic in the UK. This is what the Chief Medical Officer had to say:

"Professor Whitty said that the peak of an outbreak was expected in about two months, with 50 per cent of cases over a three-week period and 95 per cent over a nine-week period."

Mapping this on to the normal distribution gives us a standard deviation of two and a quarter weeks (σ =2.29, call it 2.25).

Fifty percent of cases would be within two thirds of a standard deviation from the central point, which gives 2 * (2/3) * (2.25) =  3 weeks. 

So the peak of cases would be two months time, early May: we are currently about three and a half standard deviations out (7.9 weeks).

Five weeks after the peak the epidemic should have burned itself out in the UK: mid-June.

So to summarise for the UK:

1. Crisis (50%):  end-April to first half of May (3 weeks)
2. Peak:               first week of May
3. Burn-out:        mid-June.

 The power of stats.
---

John Cook on automated theorem provers

(Source)

Mathematician and computer scientist John Cook restates the orthodoxy on automated theorem proving (ATP).

"When I first heard of automated theorem proving, I imagined computers being programmed to search for mathematical theorems interesting to a wide audience. Maybe that’s what a few of the pioneers in the area had in mind too, but that’s not how things developed.

The biggest uses for automated theorem proving have been highly specialized applications, not mathematically interesting theorems. Computer chip manufacturers use formal methods to verify that given certain inputs their chips produce certain outputs. Compiler writers use formal methods to verify that their software does the right thing. A theorem saying your product behaves correctly is very valuable to you and your customers, but nobody else. These aren’t the kinds of theorems that anyone would cite the way they might site the Pythagorean theorem. Nobody would ever say “And therefore, by the theorem showing that this particular pacemaker will not fall into certain error modes, I now prove this result unrelated to pacemakers.”

Automated theorem provers are important in these highly specialized applications in part because the results are of such limited interest. For every theorem of wide mathematical interest, there are a large number of mathematicians who are searching for a proof or who are willing to scrutinize a proposed proof. A theorem saying that a piece of electronics performs correctly appeals to only the tiniest audience, and yet is probably much easier (for a computer) to prove.

The term “automated theorem proving” is overloaded to mean a couple things. It’s used broadly to include any use of computing in proving theorems, and it’s used more narrowly to mean software that searches for proofs or even new theorems. Most theorem provers in the broad sense are not automated theorem provers in the more narrow sense but rather proof assistants. They verify proofs rather than discover them. (There’s some gray zone. They may search on a small scale, looking for a way to prove a minor narrow result, but not search for the entire proof to a big theorem.) There have been computer-verified proofs of important mathematical theorems, such as the Feit-Thompson theorem from group theory, but I’m not aware of any generally interesting discoveries that have come out of a theorem prover."

However, if you widen the discussion to automated deduction as we see in expert systems, planning systems and pretty much everything Google is trying to achieve, inference is everywhere.