Создание математической библиотеки будущего

[NeoCode]

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

[sgjurano]

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

[wibbtwo]

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