Do we currently know a polynomial-size Frege proof for Tseitin formulas?

Question

There's a vast literature about super-polynomial lower bounds on proof lengths of Tseitin formulas in bounded-depth Frege systems, but what I'm curious about is: what if we don't restrict the depth of the proof? I found a paper which claims that Tseitin formulas have a polynomial-size proof in the R(lin) (Resolution over Linear Equations) proof system, which was found to p-simulate Frege systems, but the author didn't mention whether Frege systems p-simulate R(lin). So, do we currenly know a concrete polynomial-size proof of Tseitin formulas in unbounded-depth Frege systems?

Answer 1

Section 6 of the following paper has a sketch:

Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209–219, 1987. DOI: https://doi.org/10.1145/7531.8928

Answer 2

Tseitin tautologies are unsatisfiable systems of linear equations over $\mathbb F_2$, and as such they can be refuted just by summing all the equations together (possibly after reconstructing the equations from a CNF encoding, depending on how exactly they are formulated). This provides a trivial proof in $\mathrm{Res}(\oplus)$ (resolution with linear equations over $\mathbb F_2$, i.e., parities of sets of literals), which is a subsystem of $F_d(\oplus)$ (constant-depth Frege with parity gates), which is p-simulated by Frege. The crux of the Frege proof is to take polynomial-size formulas for parity, and construct short proofs of their basic properties.