Build Your Own Proof Assistant course is going nicely. Still every class I cannot get people to leave once the class ends. They want to stay and keep collaborating.

The three initial teams exploring in parallel the three choices of foundations we are choosing from for our Euclidean geometry proof assistant (E, Hilbert, Tarski) are all making other fundamentally different design decisions (logic vs. type theory, LCF-style vs. classic de Bruijn style) and I'm super psyched for the discussion we have at the end of next week about those decisions and their tradeoffs.

After that we'll converge on one kernel and probably build it next sprint.

I rotate and help teams, but in between when I don't want to stress people out by hovering, I read Euclid’s Elements.