象牙の塔4階2号室

アスペとADHDの高専生によるブログ(不定期更新)

September 4th いろいろ

日記

 今日は大学編入の数学の問題集とTOEICにおける文法問題の問題集を買った。しかし忙しかったので未だ手をつけれていない。

 勉強の方はモチベーションを維持出来そうにないというか数学していたのでTOEIC対策ができてない

 その数学について、久しぶりに証明支援系のシステムであるLeanを触っていた。

www.ma.imperial.ac.uk

 このサイトで0を含む自然数における加法や乗法の公式をLeanを用いて証明できる。自然数というのには元よりペアノの公理という、証明がなくそのまま使わないと話が始まらないものが課されている。一方でa+b=b+aの可換則や(a+b)+c=a+(b+c)という結合則と呼ばれるものなどについてはペアノの公理に加えて最低限の公理で証明できる。なお、ペアノの公理数学的帰納法は基づいているため実は数学的帰納法というのは割りとプリミティブに近い技法でもある。