8 июля пройдёт следующий семинар Математического центра в Академгородке

Системы автоматизации и верификации математических доказательств работают "снизу вверх": от базовых кирпичиков к более сложным утверждениям, создаваемым практически вручную. А можно ли пойти "сверху вниз": от корпуса математических текстов по пути постепенной, пусть и частичной, формализации? Можно ли искать утверждения не по ключевым словам, а по логическому смыслу? 

Предлагаем обсудить возможные подходы к такой задаче, их реализуемость, а также существующие инструменты в этой области. 

Например, с лингвистической точки зрения математический текст состоит из относительно стандартных конструкций, обладает малой вариабельностью и лишён большинства средств выразительности и многих видов неопределённости. Вместе с тем математика является крупнейшей областью, в которой применим глубокий семантический анализ. Эти особенности позволяют надеяться на продуктивность лингвистического анализа математических текстов для поиска логических взаимосвязей и формализации доказательств.