У меня, как у непрофессонала, такой вопрос по работе Владимира Александровича по унивалентным основаниям математики. В ЖЖ опубликовали
интервью с Владимиром Воеводским:
Цитата:
И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется "унивалентные основания математики" и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут "понимать" компьютеры можно считать в основном решенной.
- Как эту идеологию воспринимает современное математическое сообщество, а именно специалисты по категориям, логике, гомотопиям? Много ли обрелось соратников среди профессиональных математиков, которые готовы серьезно работать над унивалетными основаниями?
- По-разному. Соратников собралось довольно много и собирается все больше и больше. Конечно, труднее всего специалистам по логике и основаниям математики ведь фактически то что я предлагаю, сдвигает и теорию множеств, и классическую логику на вторые планы.
Означает ли это, что в математике грядет революция по значению не ниже революции Кантора и теория множеств (и мат. логика), которые являются основой практически для всей современной математики, отойдет на второй план? Или работа Владимира Александровича больше касается автоматической проверки математических доказательств и на работе большинства математиков не отразится?
