Проект Lean: Можно ли формализовать всю математику на компьютере – и нужно ли?
Стремление к строгости в математике имеет долгую и неоднозначную историю — историю, из которой математики могут извлечь уроки сейчас, когда формализуют математику в программе Lean.
Как DeepSeek создает новые (мета)математические теории
Вместо краткого введения. Активно использую в работе DeepSeek уже чуть больше двух недель, очень доволен им и в целом продуктивность и скорость работы выросли. Но рассказать хотелось бы не об этом, точнее, не совсем об этом.
