一个博客

最近在看《同构：编程中的数学》，觉得可以用lean4来写一下里面的习题，所以记录一下。

最近龙虾大火，虽然我不觉得龙虾真的能干活，以及我认为龙虾就是个能控制电脑的聊天机器人，虽然不看好龙虾，但是咱二次元可以不养龙虾，我们可以养猫娘。

历时一个月，终于在昨天收到了在亚马逊上买的美少女万华镜15周年OST，这也是我第一次在海外买东西，所以值得记录一下。

目前为止见过的最难的，最不容易想到的题目

我证出来啦！！！

今天一个学弟拿了个有点意思的东西来给我看，问我知不知道原理，所以来试着破解一下，记录一下过程。

此为用C++写微分方程数值解实验的前置，目标是封装个多维数组，重载四则运算，实现一些矩阵的操作。

密码学大作业需要用到质数表，所以就把优雅的生成质数表作为我的第一个练习。标题叫优雅的生成质数表，不叫高效的生成质数表，所以只是用的最朴素的方法，尽可能把它写得好看，并不是最高效的生成质数表的方法。

玩了一个多月了准备回坑。

由于前段时间接触了一下lean4，所以就想着能不能用lean4来证明一下欧几里得算法能够求出最大公约数。