{'fraction_non_alphanumeric': 0.022247905229702398, 'fraction_numerical': 0.0037561398439757295, 'mean_word_length': 5.709302325581396, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
2 General Research Area – Short Background Proof complexity

My research centers around the interface between computational complexity and computational logic, with an emphasis on propositional and algebraic proof complexity. Computational complexity aims at understanding the nature and limitations of efficient computation; logic, on the other hand, and in particular proof theory, studies what can formally be proved from a given set of axioms and deduction rules, in a given language. Accordingly, proof complexity aims at characterizing which statements can formally be proved with efficient (or feasible) proofs, in a given proof system. Here the term “efficient” typically stands for two separate (though interconnected) meanings: The first meaning refers to the size of the proofs, that is, the number of symbols (or bits) it takes to write down the proofs. The second meaning refers to the efficiency of the ‘concepts’ one reasons with (the technical interpretation being the complexity class from which proof-lines are taken from). My work in proof complexity was devoted mainly to the formalization and analysis of new frameworks for providing proofs of propositional tautologies. My main contributions in that respect were in introducing and studying the notion of multilinear-proofs in Raz & Tzameret (2006), which are proof systems based on algebraic reasoning operating with multilinear arithmetic formulas; the further analysis and study of multilinear-proofs and their relations to simple proof systems combining logical and counting constructions (that is, extensions of resolution that operate with disjunctions of linear equations) in Raz & Tzameret (2007); and the introduction and complexity-theoretic study of propositional proof systems ‘carrying certain approximations’ in Dershowitz & Tzameret (2007). My current research project aims at understanding basic properties of general algebraic proof systems operating with arithmetic formulas, and specifically in providing a natural framework for obtaining lower bounds on certain such algebraic proofs. This new line of research is inspired by analogous results in traditional propositional logic and by recent important advances in algebraic circuit complexity. To some extent, traditional study in algebraic proof complexity ignored these fundamental issues, and so I believe that this program carries a considerable promise for success in the near future. My long-run research plan is to continue tackling fundamental problems in computational complexity and computational logic, by gradually expanding my fields of interest and my command of available notions and techniques from combinatorics, logic and algebra. In particular, I am consciously moving into the theory of (computational) pseudo-randomness, derandomization and hardness-versus-randomness — concentrating on its interplay with propositional proof complexity. I am also planning to continue studying propositional and algebraic proof complexity and algebraic complexity at large. I believe that fundamental questions in computational complexity are tightly linked to problems in the theory of feasible proofs, and studying the latter problems with techniques borrowing from different parts of mathematics and computer science can help in resolving (or at least greatly advance our understanding of) fundamental questions in complexity theory, which are central to any rigorous investigation in the science of computing.