Компьютерные доказательства // Лев Беклемишев

Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок. Лев Беклемишев — доктор физико-математических наук, член-корреспондент РАН, главный научный сотрудник Математического института им. В.А. Стеклова РАН, профессор факультета математика ВШЭ.