Этот текст является слегка отредактированной стенограммой содоклада на совместном заседании Санкт-Петербургского Математического общества и Секции математики Дома учёных 23 марта 2010 года. Материалы заседания, включая видеозаписи, доступны в [1].

This publication is a slightly edited verbatim report of author's co-talk presented at joint meeting of St.Petersburg Mathematical Society and Mathematical section of the House of Scientists on March 23, 2010; related materials, including video recording, can be found on [1].

Алгоритм Тарского позволяет установить истинность или ложность любого утвержения про конечное количество вещественных чисел. Вместе с методом координат Декарта это позволяет автоматически доказывать широкий класс теорем элементарной геометрии. Изложенный здесь вариант алгоритма предназначен для первоначального знакомства с этой областью - его нетрудно понять, несложно запрограммировать, но полученная программа будет крайне неэффективной.

Tarskis algorithm allows to determine whether a given statement about a finite set of real numbers is true of false. Together with the Cartesian coordinate system, it allows to prove automatically a large class of theorems of elementary geometry. The version of the algorithm presented here is suitable for introduction to the subject - it is not difficult to understand the algorithm, it is easy to write a program, but it would be extremely inefficient.