@xenaproject This might be a dumb question (albeit one that I'm unlikely to be alone in asking), but what's the current state of the art in formalized arithmetic geometry?