公益活动提议：数学证明与编程结合——自然数游戏体验课-园所风采-幼师课件网

【幼师宝】2000多G内容，终身免费更新 | 快来体验【智能幼师】，感受智能魅力！

（一）定义公益活动

公益活动由报名者众筹，共同委托承办方承办的方式展开。
承办方不以谋利为目的，也不自己倒贴钱来操办；承办方要准备场地、大屏或白板等。收支向所有参与者公开。
承办方为主讲人或嘉宾提供基本补贴，例如一次50元~200元不等，备课辛苦费；主讲人或嘉宾拿课件内容换补贴。
承办方负责去拉第三方赞助。赞助款或赞助物品抵补报名参与者自掏入场费用。也就是说，报名者可以是免费参加，但必须明白，是何人代自己负担了费用。

本活动内容：由蒲老师引导参与者通关自然数游戏训练关的8个关卡。第8关大BOSS是证明“2+2=4”。晓得这个结论不重要，重要在于尝试从更基本的定理一步步推导出这个结论。因为，数学一词的本意是要能从已知推导出新知。

活动内容适合混龄、亲子。具体活动内容参看下文，方便参与者自行判断是否适合自己。蒲老师会用点与箭头的图式来与参与者沟通，看图说话即可。

自然数游戏是经典的Lean入门游戏。适合在电脑、在平板、在手机上玩，参与者自带设备、自带纸笔、笔记本。

（二）交互式定理证明器 Lean 介绍

Lean 是一种交互式定理证明器（Interactive Theorem Prover）。它既是一个数学证明工具，也是一个功能强大的编程语言。Lean 的核心目标是帮助用户以严谨的数学语言编写定义、定理和证明，并通过计算机验证其正确性。简单来说，它就像一个“数学助手”，能让人类与计算机协作，探索和验证数学的逻辑结构。

对于家长，Lean 提供了一种让孩子接触前沿科技与数学的机会。它不仅能提升数学成绩，还能为未来的 STEM（科学、技术、工程、数学）学习打下基础。

Lean 提供了一种全新的学习数学的方式。学生可以通过编写证明来理解数学概念，比如“为什么 2 + 2 = 4”。它强调逻辑推理和严谨性，帮助学生从“知道结果”转向“理解过程”。

Lean 不仅限于数学证明，它还是一个功能完备的编程语言。学生可以用它编写程序，同时学习逻辑思维和计算机科学基础。

（三）自然数游戏

Lean 的著名入门游戏“Natural Number Game”（自然数游戏）就是一个例子。玩家通过闯关的方式，从零开始构建自然数的运算和性质（如加法、对称性），逐步掌握证明技巧。这种游戏化学习特别适合激发中小学生的兴趣。

自然数游戏是一个免费的在线游戏，适合初学者（包括中小学生和家长）。它从最基本的自然数开始，逐步引导用户学习 Lean 的操作和证明方法。

访问网址：https://adam.math.hhu.de/#/g/leanprover-community/nng4

游戏界面是这个样子：

不用怕，蒲老师会用图式来让小同学们理解。

（四）自然数游戏训练关

训练关1：rfl

rfl是reflexivity（自反性）的缩写，对应恒等态射结构（identity morphism），叫什么名字不重要，看图即可——箭头从自身出发又射回到自身。

训练关2：rw

rw是rewriting（改写）的缩写，表达转换的意思。

一支飞箭，从“源点”射出，射向“靶点”。将“源形态”转换表达为“靶形态”，同时保持某种不变性。

训练关3：rw的复合与分解

0是自然数，1是0的下个自然数，2是1的下个自然数，2是0的下下个自然数。

每个自然数都有它的下个自然数，称为它的后续（successor，缩写为succ）

训练关4：rw的反向

正向箭头，将1转换表达为0的后续；

反向箭头，将0的后续转换表达为1。

训练关5：Adding zero

例如，图式 (1+0)→1，通过rw[add_zero]，将(1+0)转换表达为1。

1+0=1，可以帮助小孩子理解。

训练关6：Precision rewriting

rw[add_zero]外加指定参数，精准定位处理。

例如，rw[add_zero c]，将(c+0)转换表达为c。

c+0=c，可以帮助理解

训练关7：add_succ

例如，rw[add_succ]，将 (1+succ 0) 转换表达为 succ (1+0)

训练关8：证明2+2=4

我们要用上述知识，一步一步将 (2+2) 转换表达为 4。

欢迎一起来挑战闯关！有意参与者加微信 hei_cuo，大家建群沟通。

文章转载自微信公众号：兼际的诗行

-=||=-收藏赞 (0)

幼儿园研学培训，找优师教研18610206462

南通、常州、成都、广州、杭州多处培训基地，优质的专家师资资源、幼儿园资源，让你深入幼儿园，近距离感受先进的幼儿园生活。专题研修：课程叙事专题研修、课程游戏化专题研修、民族特色民族文化的专题研修以及各类您需要的定制化专题学习。

公益活动提议：数学证明与编程结合——自然数游戏体验课

课件下载

置顶推荐

热门文章

切换注册登录

切换登录注册