Стремление сделать математику строгой имеет долгую и неоднозначную историю — историю, из которой математики могут извлечь уроки, стремясь формализовать всё в компьютерной программе Lean.