ParentFull threadndrwnaguib·Yes; the goal is to finish the first volume. I am particularly looking forward to formalizing the well-known 1+1 proof.View on HN