一个博客

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

因为安装和编译很多东西都需要高版本的GCC，所以折腾了一下高版本的GCC。

安装完lean4，当然要试着用一下，由于我也快两年没碰算法了，所有算法几乎都忘完了，就只记得GCD了，所以就写个GCD吧。某种程度上选择GCD说不定刚好，够经典，够简单，够数学。

突然又想玩lean4了，但是打开vscode之后不知道什么原因，我之前的lean4的环境又不能用了，vscode的自动安装又经常连不上，所以重新安装一次，顺便记录一下。

就是把整个minconda3移动到其他地方，并且还能正常使用，不是导出conda环境。

这篇文章是我无聊刷知乎的时候看见一篇用ffmpeg分离音频的文章之后，觉得这个小技巧可能挺有用，所以写的。

前几天初赛结束了，虽然成绩很不理想，但是还是进复赛了，复赛题目跟初赛就完全不一样了，希望能进决赛吧。

前段时间马斯克的Grok的AI女友火了，虽然我也很想试试但是毕竟国内，不方便使用，而且还要每月30美元，我这种喜欢白嫖的肯定就不抢先体验了（而且主要是感觉Ani长得不太符合我XP）。但是我这个人还是比较喜欢表面，或许我不需要它会说话能帮我解决问题，我想要的可能只是一个会动的二次元模型，于是几经辗转之下我找到了一个VRM桌宠，MateEngine。

CE修改器应该算是比较简单也比较通用的修改器，就是那种读取内存然后对内存进行修改的软件，理论上对大部分单机游戏都有效，但是这个软件的安装有坑。

最近太忙了都没有写博客，但是这篇觉得还是可以记录一下，所以简单的记录一下。