网站制作大连,wordpress迁移换域名,成都建设信息网官网,百度口碑视频链接#xff1a;
人工智能数学验证工具LEAN4【入门介绍5】推理世界-如何使用和证明推理性的命题_哔哩哔哩_bilibili import Game.Levels.Implication.L10one_ne_zero
World Implication Level 11 Title 2 2 ≠ 5
LemmaTab Peano …视频链接
人工智能数学验证工具LEAN4【入门介绍5】推理世界-如何使用和证明推理性的命题_哔哩哔哩_bilibili import Game.Levels.Implication.L10one_ne_zero
World Implication Level 11 Title 2 2 ≠ 5
LemmaTab Peano
namespace MyNat
Introduction 2 2 ≠ 5 is boring to prove in full, given only the tools we have currently. To make it a bit less painful, I have unfolded all of the numerals for you. See if you can use zero_ne_succ and succ_inj to prove this.
/-- $22≠5$. -/ Statement : succ (succ 0) succ (succ 0) ≠ succ (succ (succ (succ (succ 0)))) : by intro h rw [add_succ, add_succ, add_zero] at h repeat apply succ_inj at h apply zero_ne_succ at h exact h
Conclusion Heres my proof: intro h rw [add_succ, add_succ, add_zero] at h repeat apply succ_inj at h apply zero_ne_succ at h exact h
Even though Lean is a theorem prover, right now its pretty clear that we have not developed enough material to make it an adequate calculator. In Algorithm World, a more computer-sciency world, we will develop machinery which makes questions like this much easier, and goals like $20 20 ≠ 41$ feasible. Alternatively you can do more mathematics in Advanced Addition World, where we prove the lemmas needed to get a working theory of inequalities. Click \Leave World\ and decide your route.
