Something to do during your logical self-isolation: find out a little about The Lean Theorem Prover.
I confess I have previously never really “got” the supposed attractions of the likes of Coq. But I stumbled a week or two back over a piece by Thomas Hales on the pros and cons of using the much more recent Lean. There are a lot of cons, but still I was prompted to take a first quick look at the Lean documentation, and then stayed to read on quite far. As you might have predicted of something which Jeremy Avigad has a major hand in, this is really very well written. If you (like me) start with only a shaky grasp on why working in a version of dependent type theory might be a Good Thing, then this is interesting and genuinely illuminating –well worth looking at, even if you don’t find yourself playing with Lean itself for very long.