数学を厳密にするための探求は、長く、むらのある歴史を持っています。数学者たちは、コンピュータプログラムLeanで全てを形式化しようと努力する中で、この歴史から学ぶことができます。