18-JUN-2026

1251

I started this a couple days back, aiming to do something a little closer to the Mathlib standard and also get a handle on the necessary CT to get to sheaves, which I think will play back into the GIYF work around handling Lines/Tangles/the like.

So far I really like the book. I’ve taken a couple survey passes over it in the past, and Vakil’s writing style is nice, and the commitment to a sane numbering system (or, at least, sane-up-to-1.2.*, there is a lot of book here) is pretty nice. It is going to be a testbed for a new iteration of atlas’ syntax and hopefully should help drive out some more of its features.