ご無沙汰しております．
最近，定理証明支援系の Lean に興味が出てきて，ちょっと勉強しています．
定番（らしい）の Natural Number Game をまずやりましたが，「その tactic はまだ開放していないから使えないよ！」というエラーが出まくって進めなくなったので，別のチュートリアルを始めました．
整数論の定理を示してみたいですね．
今のところ簡単な四則演算をいじるくらいしかできませんが，この教材が終わるころにはどれくらいできるようになっているでしょうか…．
ご無沙汰しております．
最近，定理証明支援系の Lean に興味が出てきて，ちょっと勉強しています．
定番（らしい）の Natural Number Game をまずやりましたが，「その tactic はまだ開放していないから使えないよ！」というエラーが出まくって進めなくなったので，別のチュートリアルを始めました．
整数論の定理を示してみたいですね．
今のところ簡単な四則演算をいじるくらいしかできませんが，この教材が終わるころにはどれくらいできるようになっているでしょうか…．