Как стать автором
Обновить

Комментарии 3

Это круто. Я к сожалению не математик, но интуитивно понимаю, что это исключительно правильное направление движения. Компьютеры должны уметь обращаться с информацией на как можно более глубоком семантическом уровне, а не просто гонять по сети гигабайты «человекоориентированного» видео, которое для самих компьютеров по сути информационный шум.
Вот когда подобным образом будет оцифрована не только математическая информация, но и информация из множества других областей знаний, тогда и наступит Сингулярность.

Principia Mathematica 2, Рассел помнится писал, что жалеет о времени потраченном на этот труд.

Неудивительно, учитывая, что General Problem Solver уже в 1957 году доказал большую часть теорем из Principia Mathematica по-сути простым поиском по дереву. Не совсем понятно, чем этот Lean лучше GPS?

Зарегистрируйтесь на Хабре, чтобы оставить комментарий

Публикации

Изменить настройки темы

Истории