Twitterで「ベクトルを使うと5秒位で余弦定理証明できるので良い」 とあったので、Idris, Leanでチャレンジしてみた。 参考記事： ちなみに、余弦定理の証明に、 （成分表示で証明した）内積の分配法則を 使ってしまうと循環論法になるそうです。 自分は仮定…