| 13759 |      1 | finish converting ZF to new-style theories
 | 
|  |      2 | add the SET protocol proofs to HOL/Auth
 | 
|  |      3 | add Quadratic Reciprocity
 | 
|  |      4 | complete the new formalization of Group theory
 | 
|  |      5 | 
 | 
|  |      6 | add Presburger arithmetic (if possible until March)
 | 
| 13761 |      7 | stop eta-contraction for binders
 |