本预找回高中时的一份数学笔记，反而促使我开始回忆那段长达6年的中学时光，深夜有感，零零碎碎拼凑得此篇。
我的语文不是很好，我并不擅长预习。小学老师说有时候他喜欢写一些人生随笔，而我看着作文本上的“题记”二字不知道如何预习人生。
我的语文不是很好，老师们常常这么说。我总是理不清拐弯抹角的题干，分不清“意义”与“作用”
关于人在不想干正事的时候能干出啥来。。。
第一次记录：2024年12月24日丑时
有不少 Bug，稳定性可能不是很好，但是很爽！（比如优先级问题）
项目结构如下！
MrMath├─ ...├─ Cargo.lock├─ Cargo.toml└─ src ├─ backend │ ├─ ast.rs
后续：这个代码发现还是有不少问题的，但是博主很懒，所以有空再把调整后的代码放上来吧~
前天学习了如何使用 rust，想随便写点东西练练手，就想着写一个简单的 Math Repl 吧。这是第一版（对的，还有第零版）的某个数学运算组件，正好没考虑效率地写完了可以进行测试，于是就有了这篇博客。
背景故事：第零版写着写着
不必先安装 Visual Studio，可以直接安装 Rust。建议先安装 MinGW64（ucrt），然后选择 rustup-init 的选项 2 自行配置。点击跳转参考1，点击跳转参考2
建议检查一下 gcc 版本，别太低了。。。（与安全选项有关）
调整安装路径。方法：自行配置环境变量 RUSTUP_H
本次比赛是笔者主导发起的、学校本科的第一场本科部级的CTF比赛，笔者共出了 5 个Welcome题目，1 个 Pwn题（UAF+堆管理），3.5 个 Misc （1 个 AI模型题、1 个音频隐写、1 个文件格式题、0.5 个社会工程题）和 6 个 Crypto。下面给出其中两个 Crypto 题目的解题思路。
上一篇：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