An obvious approach to explaining NP != coNP, how far has it been pushed?
Not very far. The approach that you are describing is known as proof complexity, and it is covered by several surveys and lecture notes. There are several kinds of proof system being considered:


Frege systems. These are systems in which a proof consists of a sequence of formulas or circuits (depending on the system), and there is a fixed set of derivation rules.
Algebraic proof systems such as the Polynomial Calculus and Nullstellensatz. Here each line is a polynomial.
Cutting planes, in which each line is a linear inequality.


There are also other proof systems such as the Hajos calculus, a proof system for proving that a graph isn't 3-colorable.

We have strong lower bounds for some of these systems, but in the Frege front, the best lower bound is for bounded depth Frege, in which the depth of all lines in the proof is bounded by some constant. This lower bound is similar in some regards to AC0 lower bounds for circuits, but is otherwise more complicated. We have no lower bound for the version in which the depth is bounded but we allow mod $p$ gates; the algebraic methods used to prove lower bounds on circuits don't seem to work, and the problem seems related to derandomizing polynomial identity testing, a notoriously difficult problem in algebraic complexity theory.

The Frege proof system itself has as lines arbitrary formulas, and Extended Frege has arbitrary circuits as lines. It is thought that Extended Frege is stronger than Frege. Other proof systems are conjectured to be stronger than even Extended Frege. It is not clear currently whether there is a "super" proof system, which is optimal up to polynomial factors compared to any proof system. Thus even if we do manage to prove lower bounds for progressively more general proof systems – which is expected to be harder than proving corresponding circuit lower bounds – we wouldn't necessarily be able to prove that NP is different from coNP in this way.