extremal_graph Turan's theorem is one of the basic results of extremal graph theory so I thought it might be a good place to start if I wanted to learn Lean. Main theorem(s) are in https://github.com/jt496/extremal_graph/blob/master/src/theorems.lean