Mechanical Geometry Theorem Proving

[nnosipov]

В этой теме предлагается обсуждать различные вопросы, относящиеся к доказательству теорем геометрии методами компьютерной алгебры. Прилагаю препринт моей статьи "О механическом доказательстве планиметрических теорем рационального типа" (журнал "Программирование", 2013). Было бы интересно увидеть замечания, комментарии и т.п. по теме статьи.

Аннотация. В статье предлагается элементарный подход к механическому доказательству планиметрических теорем рационального типа. Это подход реализован в виде программных модулей geom и его модифицированной версии geom_zeta, созданных в системе компьютерной алгебры Maple. Приводятся многочисленные примеры механических доказательств сложных теорем планиметрии (как хорошо известных, так и сравнительно новых) на основе удобных рациональных параметризаций.

Ниже приводятся ссылки на некоторые темы форума, где можно увидеть примеры механического доказательства теорем планиметрии:

Диагонали вписанного шестиугольника
Треугольник и три центра описанных окружностей
Орбиты Жукова
Подобные равнобедренные треугольники
Обсуждение и разбор марафонских задач-ММ157
Задача на построение
Очень сложная геометрическая задача
Гипотеза о трёх параболах

[nnosipov]

Вот ещё несколько текстов (файлы Mechanical-Geometry-Theorem-Proving-1.pdf, Mechanical-Geometry-Theorem-Proving-2.pdf, theorem-about-incenters.pdf) с многочисленными примерами механического доказательства (решения) планиметрических теорем (задач). Эти тексты более элементарны и вполне доступны школьникам.

[nnosipov]

Вот пример задачи рационального типа с "внешними" условиями (выделено жирным шрифтом).

В треугольнике $ABC$ с углом $\angle BAC=60^\circ$ проведена биссектриса $BD$ и затем продолжена до пересечения в точке $S$ с описанной окружностью. Пусть $K$ --- вторая точка пересечения прямой $AB$ с окружностью, описанной около треугольника $ADS$. Найдите $|BC|$, если $|AB|=8$ и $|AK|=1$.

Чтобы решить эту задачу механически, сначала переформулируем её: будем искать $|BC|/|AK|$ при условии $|AB|/|AK|=8$. Далее можно применить $T_aT_bT_c$-параметризацию: $T_a=z_1$, $T_b=1$, $T_c=\zeta=\cos{120^\circ}+i\sin{120^\circ}$. Следующие вычисления проделаны с помощью модуля geom_zeta:

$$ A=2\eta^2, \quad B=\frac{2(\eta^2-1)z_1}{z_1-1+\eta^2}, \quad C=\frac{2z_1}{z_1+1}, \quad D=\frac{2z_1}{z_1-\eta^2}, \quad O=\frac{2\eta^2z_1(z_1+\eta^2)}{(z_1-1+\eta^2)(z_1+1)}, \quad S=\frac{2\eta^2z_1}{z_1+1}, $$

$$ O_1=\frac{2\eta^2z_1(z_1+1-\eta^2)}{(z_1-\eta^2)(z_1+1)}, \quad K=\frac{2(\eta^2-1)z_1}{z_1+1} $$

($O$ и $O_1$ --- центры описанных окружностей треугольников $ABC$ и $ADS$ соответственно). Теперь имеем $|AB|^2/|AK|^2-64=f(z_1)/g(z_1)$, где

$$ f(z_1)=441z_1^4+(-896+1792\eta^2)z_1^3-2226z_1^2+(896-1792\eta^2)z_1+441. $$

Осталось вычислить

$$ a=\frac{|BC|^2}{|AK|^2}=-\frac{3z_1^2}{(z_1-1+\eta^2)^2(z_1+\eta^2)^2} $$

при условии $f(z_1)=0$. Пусть $h(z_1)$ --- числитель дроби $|BC|^2/|AK|^2-a$. Результант многочленов $f(z_1)$ и $h(z_1)$ равен $194481(a-49)^2(a-81)^2$. Таким образом, $a=49$ или $a=81$. Отсюда ответ к задаче: $|BC|=7$ или $|BC|=9$ (можно показать, что оба варианта реализуются).

[nnosipov]

Вот ещё один пример теоремы с "внешним" условием (на это раз условие имеет вид равенства с дополнительными ограничениями типа неравенств, т.е. по существу не является алгебраическим).

Если в треугольнике $ABC$ две чевианы $BB_1$ и $CC_1$ равны, а их точка пересечения лежит на биссектрисе угла при вершине $A$, то треугольник $ABC$ --- равнобедренный.

Пусть $A=0$, а $P=1$ --- общая точка чевиан $BB_1$ и $CC_1$. Положим $C=bz_1$, $B=cz_1^{-1}$, где $z_1+z_1^{-1}=2\cos{\phi}>0$. Тогда

$$ B_1=\frac{cz_1^2}{cz_1^2-z_1+c}, \quad C_1=\frac{b}{bz_1^2-z_1+b}, \quad Q=\frac{bc(z_1^2+1)}{(b+c)z_1}, $$

где $Q>1$ --- основание биссектрисы. Вычислив $|BB_1|^2-|CC_1|^2$ и приравняв к нулю, мы получим либо $b=c$ (что нам и нужно), либо $z_1^2bc-bz_1+bc-cz_1=0$ (что равносильно равенству $Q=1$ и потому невозможно), либо

$$ 4bc\cos{\phi}+\frac{b^2+c^2+1}{\cos{\phi}}=2(b+c)(bc+1). \eqno(*) $$

Последнее равенство также невозможно. Действительно, из неравенства $Q>1$ следует, что

$$ 1>\cos{\phi}>\frac{b+c}{2bc}. \eqno(**) $$

Отсюда $2bc>b+c$ и, как следствие, $b+c>1$. На интервале $(**)$ левая часть $(*)$ как функция $\cos{\phi}$ является выпуклой и, как нетрудно убедиться, на концах этого интервала меньше правой части. Поэтому левая часть $(*)$ всюду меньше правой.

Геометрическое доказательство этой теоремы (обобщающей известную теорему Штейнера-Лемуса) см. в журнале "Математика в школе", 1948, № 1.