Проект Lean: Можно ли формализовать всю математику на компьютере – и нужно ли?
Стремление к строгости в математике имеет долгую и неоднозначную историю — историю, из которой математики могут извлечь уроки сейчас, когда формализуют математику в программе Lean.
