Big notation Propositional Formulas

Question

I am reading a lecture and there is a sentece that say:

Every tautology $\tau$ on $n$ variables has an proof in which there are at most $2^{O(n)}$ formulas.

I know that $O$ is the big notation used for the worst case in algorithms, but in this case What means that? Could you give an example please?

Answer 1

The notation $O(n)$ means the same thing here as there: Some function of $n$ which is no larger than $Cn$ for some $C$. So that sentence means that there exists $C$ such that every tautology in $n$ variables has a proof with no more than $2^{Cn}$ steps.