lean4专题
人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界：逆否策略的等效替代，提取假设 的已知，tauto另类理解，更 严格的归纳法假设。。。
视频讲解：人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界：逆否策略的等效替代，提取假设 的已知，tauto另类理解，更 严格的归纳法假设。。。_哔哩哔哩_bilibili import Game.Levels.AdvMultiplication.L08mul_eq_zero World "AdvMultiplication" Level 9 Title "mul_left_can
人工智能数学验证工具LEAN4【入门介绍7】高级加法世界-如何进行分类讨论
视频链接：人工智能数学验证工具LEAN4【入门介绍7】高级加法世界-如何进行分类讨论_哔哩哔哩_bilibili import Game.Levels.AdvAddition.L05add_right_eq_zero World "AdvAddition" Level 6 Title "add_left_eq_zero" TheoremTab "+" namespace MyNat
人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理
视频链接，创作不易记得投币：人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理_哔哩哔哩_bilibili import Game.Levels.Power.L09add_sq World "Power" Level 10 Title "Fermat's Last Theorem" namespace MyNat Introduction " We now hav