О языках геометрии и понимании геометрических фактов

В начале доклада будет упомянут незавершённый проект Воеводского, в котором предполагалось существенно расширить взаимодействие математиков c компьютерами при построении и проверке доказательств; основное внимание будет уделено языковым аспектам проекта. Основная часть доклада будет посвящена геометрии. Будет рассказано о её пяти языках, которыев последние годы изучаются докладчиком совместно с лингвистом Г.Е. Крейдлиным. Мы рассмотрим проблемы выразимости,формализации и переводов. Речь пойдёт о природе ПОНИМАНИЯ геометрических фактов, а такжевыбору наилучших (наиболее понятных) формулировок из множества равносильных. На классических примерах будут сопоставлены формальные доказательства и интуитивно убедительные объяснения наблюдаемых явлений. Если позволит время, будут упомянуты более сложные примеры, в которых элементарная геометрия граничит с алгебраической. В заключение будут перечислены проблемы, представляющиеся докладчику открытыми.