Recent developments in asymptotic extremal combinatorics have provided powerful automatic and semi-automatic methods for proving theorems in the dense setting. For example I will show how relying completely on a computer, one can solve an old conjecture of Erdos and answer a question of Sidorenko and of Jagger, Stovicek and Thomason. These new discoveries raise the following fundamental question: is it possible to prove every true algebraic inequalities between graph densities using a finite amount of manipulation with densities of finitely many graphs?'' Although this question itself is not well-defined, various precise refinements of it are formulated independently by Razborov and Lovasz. I will present a joint theorem with Sergey Norin which answers many of these questions.