The field of proof complexity is witnessing significant developments, with a focus on improving lower bounds for various proof systems. Researchers are exploring new techniques to establish nearly quadratic-size formula lower bounds and exponential-size sum-of-ROABPs lower bounds, pushing the boundaries of what is possible in algebraic proof complexity. In parallel, the study of orthologic is gaining traction, with applications in type systems, verification algorithms, and proof assistants. The extension of orthologic to support monotonic and antimonotonic functions, as well as the development of efficient algorithms for deciding subtyping relations and computing interpolants, are notable advancements. The creation of modern proof systems, such as LISA, and the extension of existing formats, like SC-TPTP, demonstrate the growing importance of proof assistants and automated theorem provers in the field. Noteworthy papers include:

• IPS Lower Bounds for Formulas and Sum of ROABPs, which proves nearly quadratic-size formula lower bounds for multilinear refutation.
• Interpolation and Quantifiers in Ortholattices, which presents a sequent-based proof system for quantified orthologic and shows that interpolants always exist.
• LISA -- A Modern Proof System, which introduces a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory.