Sikesibian's Blog
上一篇：Lean4-0 —— Lean4 的安装
这里假定大家有一定C语言、Python基础。
注释：单行注释：-- 注释，多行注释：/- 多行注释 -/。下面的代码中会使用注释来标记代码的解释说明或者Lean的返回结果。Lean是很方便的，它往往能实时向我们返回结果。
1. Lean4 中的声明、检查与求值
下面
下一篇：Lean4-1 —— Lean4 的基本使用
VSCode 中安装 Lean 4
VSCode中安装扩展：
跟随右侧导航走即可：
记得给 elan 设置一下环境变量，elan 一般在这个文件夹下（C:\User\<User Name>\.elan\bin\）：
编写一个测试文件：
点击右侧
听说有人在催我写博客
1. x2+y2x^2+y^2x2+y2形式的素数
考虑这样一个十分经典的问题：
对于不定方程 x2+y2=px^2+y^2=px2+y2=p，其中 ppp 为正素数，那么该方程是否存在整数解？
OK，我们把问题简化一下：
对于不定方程 x2+y2≡0(modp)x^2+y^2\equi