続編の動画が上がっていた。 インストールは手間だから https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover-community%2Ftutorials%2Fmaster%2Fsrc%2Fexercises%2F00_first_proofs.lean こ…

https://www.youtube.com/watch?v=ArGLTAjak3g YouTubeでLeanの動画があるのだけれど、 結構すごそうなので、自分でもやってみたいと思った。 拡張ライブラリmathlibを使う。 Coqに対するSSReflectのような物か。 インストール https://leanprover-community…

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

Twitterで「各桁の和が3の倍数な整数は3の倍数、定理証明の練習に良さそう」 というのがあったので、チャレンジしてみる。 sumDigitは各桁の和を求める関数だが、 ここで一つズルをする。 直接、各桁の和を求めるのではなく、再帰した時の関係性を書くのだ。…

rev_rev_idとは、リストを2回逆順にすると元に戻る、というやつだ。 Leanで挑戦してみた。 Leanのインストール バイナリがあるから、それを持ってくるだけ。 本格的にやりたい方は https://righ1113.hatenablog.com/entry/2020/06/06/101151 をどうぞ。 開発…