Заведующий отделом математической логики Института математики им. В. А. Стеклова
С 7 декабря 1991 года — член-корреспондент РАН (секция математики, механики, информатики)
С 25 мая 2000 года — академик РАН
Математическая логика
В 1968 году в совместной работе с П. С. Новиковым опубликовал отрицательное решение проблемы Бёрнсайда в теории групп. Создатель научной школы в области алгоритмических вопросов алгебры и логики.