Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
finish converting ZF to new-style theoriesadd the SET protocol proofs to HOL/Authadd Quadratic Reciprocitycomplete the new formalization of Group theoryadd Presburger arithmetic (if possible until March)stop eta-contraction for binders