Sidney Zhang
@lyz.one
Data Scientist | Math Lover | Chinese
Haskell · Rust · Racket
Love my wife
Haskell · Rust · Racket
Love my wife
今天自己博客的nginx服务器挂了……修了30分钟……囧……差点就让我改用Caddy了……最后还是救回来了……真的是更新更挂了一切的具象化……
November 17, 2025 at 10:00 AM
今天自己博客的nginx服务器挂了……修了30分钟……囧……差点就让我改用Caddy了……最后还是救回来了……真的是更新更挂了一切的具象化……
从近几个月开始，确实AI的新论文越来越水……国内公司更多还在更新更快更强，还有训练效率和训练模式的更新上，注意力机制现在看也有几个固定方向各有不同公司在发力。反映到论文上就感觉很水。这是不是因为快过年了？所以大家都在划水？
November 11, 2025 at 7:05 AM
从近几个月开始，确实AI的新论文越来越水……国内公司更多还在更新更快更强，还有训练效率和训练模式的更新上，注意力机制现在看也有几个固定方向各有不同公司在发力。反映到论文上就感觉很水。这是不是因为快过年了？所以大家都在划水？
有人还试图修改我的instagram密码？震惊了啊……
November 11, 2025 at 6:41 AM
有人还试图修改我的instagram密码？震惊了啊……
和我重名（拼音重叠）、还发论文的，竟然有一个了！开心！哈哈哈哈~能看到和我重名（文字完全相同）的真的太少了！
November 11, 2025 at 6:33 AM
和我重名（拼音重叠）、还发论文的，竟然有一个了！开心！哈哈哈哈~能看到和我重名（文字完全相同）的真的太少了！
为什么要学Lean4呢？我看很多数学系教授都没说清楚啊……不是形式化证明，也不是更通用的交流途径，而是给数学系学生学以致用的一个手段，这个手段不但可以验证所想，方便学习，也能干点儿简单的事，这可比R有意思多了。当然，论文画图还是不可避免的要用R或者python。
November 11, 2025 at 6:27 AM
为什么要学Lean4呢？我看很多数学系教授都没说清楚啊……不是形式化证明，也不是更通用的交流途径，而是给数学系学生学以致用的一个手段，这个手段不但可以验证所想，方便学习，也能干点儿简单的事，这可比R有意思多了。当然，论文画图还是不可避免的要用R或者python。
之前误解了scoop update的逻辑，这两天才搞懂。不用先自升级，直接 `sudo scoop update -a -g` 就可以了……白白浪费我半天时间搞好的scoop升级加清理垃圾的脚本……
November 11, 2025 at 6:23 AM
之前误解了scoop update的逻辑，这两天才搞懂。不用先自升级，直接 `sudo scoop update -a -g` 就可以了……白白浪费我半天时间搞好的scoop升级加清理垃圾的脚本……
比较来说，nushell也不错，比Bash好用，浏览数据很方便。
November 11, 2025 at 6:21 AM
比较来说，nushell也不错，比Bash好用，浏览数据很方便。
要说呢，PowerShell还是有很多好处的，比Nushell在文件操作上有更大的空间，只是提权的操作也更多就是了。
November 11, 2025 at 6:19 AM
要说呢，PowerShell还是有很多好处的，比Nushell在文件操作上有更大的空间，只是提权的操作也更多就是了。
看Stephen King高强度tweets……( ╯□╰ )
November 11, 2025 at 6:18 AM
看Stephen King高强度tweets……( ╯□╰ )
@smitechow.com 对啦~你主账号发的内容我还是看不见呢……😑
November 7, 2025 at 9:56 AM
@smitechow.com 对啦~你主账号发的内容我还是看不见呢……😑
lean4让我找回了大学时学haskell的感觉😂～
November 3, 2025 at 2:57 AM
lean4让我找回了大学时学haskell的感觉😂～
今天要猛猛的干活！顺便总结一个lean4的安装入门心得…
November 3, 2025 at 2:56 AM
今天要猛猛的干活！顺便总结一个lean4的安装入门心得…
这两天喜欢上了徐再思的散曲～怎一个好字了得～“月对芙蓉，人在帘栊。太华朝云，太液秋风。”真的是美得不得了～
November 1, 2025 at 4:52 AM
这两天喜欢上了徐再思的散曲～怎一个好字了得～“月对芙蓉，人在帘栊。太华朝云，太液秋风。”真的是美得不得了～
qwen wan.video 这次的生成效果，真的不错。就是我这免费用户，生成时长有点短……不知道付费之后，生成时长会不会增长？
https://wan.video/
<!DOCTYPE html>
<html data-theme="light">
<head>
<meta charSet="utf-8"/>
<title>Wan AI: Leading AI Video Generation Model</title>
<meta property="og:title" content="Wan AI: Leading AI Vid...
wan.video
October 28, 2025 at 2:40 AM
qwen wan.video 这次的生成效果，真的不错。就是我这免费用户，生成时长有点短……不知道付费之后，生成时长会不会增长？
21年、22年的时候，根本没学明白lean4的curry-howard同构，这次算是学的好一些了。不知道下一个ring/交换环，这次能不能搞清楚…😑我的数论学的仅及格水平的啊……
October 26, 2025 at 2:39 PM
21年、22年的时候，根本没学明白lean4的curry-howard同构，这次算是学的好一些了。不知道下一个ring/交换环，这次能不能搞清楚…😑我的数论学的仅及格水平的啊……
curry-howard同构，一样需要在lambda演算下进行，curry-howard同构更多是逻辑行为在程序过程上的同构。所以传统逻辑疑问在程序化过程中也会有类似问题被阻碍，比如np问题。那么，本质上对数学的逻辑检验也依赖于数学本身的结构逻辑化，只是在现在越来越复杂的数学结构下，curry-howard同构提供了不出错的第三方（电脑程序）进行再已知结构下的检验，这确实是一种便利。coq、lean4这些辅助证明器要是更便于非专业用户理解就好了啊～😑
October 26, 2025 at 2:30 PM
curry-howard同构，一样需要在lambda演算下进行，curry-howard同构更多是逻辑行为在程序过程上的同构。所以传统逻辑疑问在程序化过程中也会有类似问题被阻碍，比如np问题。那么，本质上对数学的逻辑检验也依赖于数学本身的结构逻辑化，只是在现在越来越复杂的数学结构下，curry-howard同构提供了不出错的第三方（电脑程序）进行再已知结构下的检验，这确实是一种便利。coq、lean4这些辅助证明器要是更便于非专业用户理解就好了啊～😑