Metamath contributions and COVID-19?

[David A. Wheeler]

Thierry Arnoux asked me an intriguing question:

> Could it be that the lock-down imposed... due to the Coronavirus
> is giving people time to progress on their Metamath proofs?

I cannot determine causes from simple counts, but I can at least determine if there are changes in rates and timings that suggest causes. I could certainly believe that some people have more time to create Metamath proofs than before.

So... I just updated the "Metamath contributions over time" graph to see if I can easily answer that question. You can see it here:
https://docs.google.com/spreadsheets/d/1TnuBekyUP918smZeJRD0WrPhJthi915Ose0cnUnB1uc

There seems to be an acceleration in the last months, simply by looking at it visually. However, the acceleration seems to have started before most confinements worldwide, so there might not be a direct correlation. In addition, the rate of theorem increase is very noisy, so just by examining it visually it is not clear that the recent acceleration is real or simply noise.

I have not done any serious statistical analysis of the data, but I do make the data public. If someone else feels like examining the data in a more serious statistical manner, I'd love to hear about it.

I hope that everyone is staying safe and healthy. I wish everyone the very best.

--- David A.Wheeler

[Jim Kingdon]

Anecdotally (and just for myself), I thought I'd have tons of time to work on metamath.

And that's sort of true, but I also realized how much of my proving happens in places like trains (and other places I'm not in these days). And there are various distractions which weren't there before.

End result? Probably not a huge increase or decrease.

In historical terms, for a while everyone was talking about how Isaac Newton was fleeing an epidemic when he wrote The Opticks. Anyone know any analogous stories for mathematics?

[Alexander van der Vekens]

I think the accelerations in the last month are not caused by COVID-19 resp. the lock-down caused by it. It was mainly Benoit, Stanislas (Open AI), Glauco (e transcedental) and me (category theory) who contributed. At least from my side, I can assure that I didn't have more time for Metamath because of COVID-19 as I would have had without it - working at home does not increase my spare time significantly.

Alexander