Is Norbert Blum's 2017 proof that $P \ne NP$ correct? Norbert Blum recently posted a 38-page proof that $P \ne NP$. Is it correct?

Also on topic: where else (on the internet) is its correctness being discussed?

Note: the focus of this question text has changed over time. See question comments for details.
As noted here before, Tardos' example clearly refutes the proof; it gives a monotone function, which agrees with CLIQUE on T0 and T1, but which lies in P. This would not be possible if the proof were correct, since the proof applies to this case too. However, can we pinpoint the mistake? Here is, from a post on the lipton's blog, what seems to be the place where the proof fails:

The single error is one subtle point in the proof of Theorem 6, namely in Step 1, on page 31 (and also 33, where the dual case is discussed) - a seemingly obvious claim that $C'_g$ contains all the corresponding clauses contained in $CNF'(g)$ etc, seems wrong. 

To explain this in more detail, we need to go into the proof and approximation method of Berg and Ulfberg, which restates the Razborov's original proof of the exponential monotone complexity for CLIQUE in terms of DNF/CNF switches. This is how I see it:

To every node/gate $g$ of a logic circuit $\beta$ (containing binary OR/AND gates only), a conjunctive normal form $CNF(g)$, a disjunctive normal form $DNF(g)$, and approximators $C^k_g$ and $D^r_g$ are attached. $CNF$ and $DNF$ are simply the corresponding disjunctive and conjunctive normal forms of the gate output. $D^r_g$ and $C^k_g$ are also disjunctive and conjunctive forms, but of some other functions, "approximating" the gate output. They are however required to have bounded number of variables in each monomial for $D^r_g$ (less than a constant r) and in each clause for $C^k_g$ (less than a constant k).

There is notion of an "error" introduced with this approximation. How is this error computed? We are only interested in some set T0 of inputs on which our total function takes value 0, and T1 of inputs on which our total function takes value 1 (a "promise") . Now at each gate, we look only at those inputs from T0 and T1, which are correctly computed (by both $DNF(g)$ and $CNF(g)$, which represent the same function - output of gate $g$ in $\beta$) at gate output, and look how many mistakes/errors are for $C^k_g$ and $D^r_g$, compared to that. If the gate is a conjunction, then the gate output might compute more inputs from T0 correctly (but the correctly computed inputs from T1 are possibly decreased). For $C^k_g$, which is defined as a simple conjunction, there are no new errors however on all of these inputs. Now, $D^r_g$ is defined as a CNF/DNF switch of $C^k_g$, so there might be a number of new errors on T0, coming from this switch. On T1 also, there are no new errors on $C^k_g$ - each error has to be present on either of gate inputs, and similarly on $D^r_g$, switch does not introduce new errors on T1. The analysis for OR gate is dual.

So the number of errors for the final approximators is bounded by number of gates in $\beta$, times the maximal possible number of errors introduced by a CNF/DNF switch (for T0), or by a DNF/CNF switch (for T1). But the total number of errors has to be "large" in at least one case (T0 or T1), since this is a property of positive conjunctive normal forms with clauses bounded by $k$, which was the key insight of Razborov's original proof (Lemma 5 in the Blum's paper).

So what did Blum do in order to deal with negations (which are pushed to the level of inputs, so the circuit $\beta$ is still containing only binary OR/AND gates)? 

His idea is to preform CNF/DNF and DNF/CNF switches restrictively, only when all variables are positive. Then the switches would work EXACTLY like in the case of Berg and Ulfberg, introducing the same amount of errors. It turns out this is the only case which needs to be considered.

So, he follows along the lines of Berg and Ulfberg, with a few distinctions. Instead of attaching $CNF(g)$, $DNF(g)$, $C^k_g$ and $D^r_g$ to each gate $g$ of circuit $\beta$, he attaches his modifications, $CNF'(g)$, $DNF'(g)$, ${C'}^k_g$ and ${D'}^r_g$, i.e. the "reduced" disjunctive and conjunctive normal forms, which he defined to differ from $CNF(g)$ and $DNF(g)$ by "absorption rule", removing negated variables from all mixed monomials/clauses (he also uses for this purpose operation denoted by R, removing some monomials/clauses entirely; as we discussed before, his somewhat informal definition of R is not really the problem, R can be made precise so it is applied at each gate but what is removed depends not only on previous two inputs but on the whole of the circuit leading up to that gate), and their approximators ${C'}^r_g$ and ${D'}^r_g$, that he also introduced. 

He concludes, in Theorem 5, that for a monotone function, reduced $CNF'$ and $DNF'$ will really compute 1 and 0 on sets T1 and T0, at root node $g_0$ (whose output is the output of the whole function in $\beta$). This theorem is, I believe, correct. 

Now comes the counting of errors. I believe the errors at each node are meant to be computed by comparing reduced $CNF'(g)$ and $DNF'(g)$ (which are now possibly two different functions), to ${C'}^r_g$ and ${D'}^k_g$ as he defined them. The definitions of approximators parrot definitions of $CNF'$ and $DNF'$ (Step 1) when mixing variables with negated ones, but when he deals with positive variables, he uses the switch like in the case of Berg and Ulfberg (Step 2). And indeed, in Step 2 he will introduce the same number of possible errors like before (it is the same switch, and all the involved variables are positive). 

But the proof is wrong in Step 1. I think Blum is confusing $\gamma_1$, $\gamma_2$, which really come, as he defined them, from previous approximators (for gates $h_1$, $h_2$), with positive parts of $CNF'_\beta(h_1)$ and $CNF'_\beta(h_2)$. There is a difference, and hence, the statement "$C_g'$ contains still all clauses contained in $CNF'_\beta(g)$ before the approximation of the gate g which use a clause in $\gamma_1'$ or $\gamma_2'$" seems to be wrong in general.