In this problem session, I will roughly share some ideas from the paper “a formal treatment of bidirectional typing”, and show some definitions (i.e. annotatability, mode-correctness) in a formal way.