Learning algorithms versus automatability of Frege systems

Ján Pich, Rahul Santhanam

We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system $P$, we…