Сложность (полу)алгебраических доказательств

Как можно доказать, что многочлены $f_1, ..., f_m$ от $n$ переменных не имеют общих корней? (В алгебраически замкнутом поле) при помощи теоремы Гильберта о нулях можно построить многочлены $g_1, ..., g_m$, которые дадут тождество $\sum f_i g_i = 1$. Почти тридцать лет назад P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi и P. Pudlák предложили рассматривать такой способ как систему доказательств для пропозициональной логики.
Однако какова будет длина таких доказательств? Можно ли их записать столь компактно, что длина будет небольшой? Можно ли сэкономить, если использовать неравенства? Ответы на эти вопросы - часть "программы С. А. Кука" для теории сложности пропозициональных доказательств, плана по получению экспоненциальных нижних оценок для всё более мощных системы доказательств. В докладе будет рассказано о нескольких вариантах (полу)алгебраических систем доказательств и их связи с гипотезами М.Шуба и С.Смейла.