$ whoami
千秋
Independent Developer
I build systems where theory has to touch real code: functional programming, formal verification, compiler experiments, graphics engines, and practical automation. Currently looking for open source or development roles in Shanghai.
$ cat contact.json
- location
- Shanghai / Remote
- github
- github.com/BreakingLead
- writing
- /blog
$ ls ./focus
- Functional programming, type systems, and dependent types
- Formal verification with Lean and proof-oriented engineering
- Low-level graphics, WebGPU, WebAssembly, and engine architecture
$ tail -n 5 ./blog
Latest Posts
- Tension Jul 29, 2026
11 音 四级 可以用于 IV 大七 FM 7 ( 11 ) : F A C E B 紧张感 由于升四度,有千与千寻的感觉(?)神秘的神隐感 可以用五级六级和弦保持这个4音 终止的一级可以加入 11 有奇妙的氛围感,很不和谐。 加在属...
/blog/04_音乐/tension - lean Jul 29, 2026
结构体默认值 haskell structure Box where m := 0 def b : Box := {} eval b { m := 0 } 默认值语法 State Monad 本文假定你对 Monad 有了解,只需要知...
/blog/05_计算机/lean - nixos Jul 29, 2026
https://nix.dev/tutorials/nixlanguage.html module 一个简化的 Nixpkgs Module 结构如下: typescript {lib, config, options, pkgs, ...
/blog/05_计算机/nixos - Hessian Matrix & SVD 分解 Jul 29, 2026
梯度告诉你往哪边走。 Hessian 告诉你每个方向弯得多厉害。 SVD 把一个线性映射拆成:正交变换、沿坐标轴伸缩、再做一次正交变换。 Hessian 描述函数的局部形状。SVD 描述矩阵怎样变形空间。二者在最小二乘中接到一起。 H...
/blog/07_数学/hessian-matrix--svd-分解 - 半角公式 Jul 29, 2026
gg (4 封私信 / 2 条消息) 半角公式的推导(超详细版) 知乎 一、半角公式 $$ \sin\frac{\alpha}{2}=\pm\sqrt{\frac{1\cos\alpha}{2}} $$ $$ \cos\frac{\a...
/blog/07_数学/半角公式