diff --git a/README.md b/README.md
index 5bafbf6..60fb70d 100644
--- a/README.md
+++ b/README.md
@@ -2,3 +2,15 @@
 
 Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
 
+## Things to do for Lean SS project
+
+Lang's algebra (revised 3rd edition) contains a chapter on general homology theory, with a section on spectral sequences. Thus, we can use this book at least as an outline for the algebraic part of the project.
+
+###To Do:
+- R-modules, vector spaces,
+- some basic theory: product, tensor, hom, projective,
+- categories of algebras, abelian categories,
+
+###Already Done:
+- definition of algebraic structures such as groups, rings, fields, 
+- some algebra: quotient, product, free.