$ 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
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

View all
  1. 初等数论笔记:整除、最大公因数与同余 Sep 19, 2026

    一、整除与最大公因数 定理 1:整除的线性组合性质 若 $$ d\mid a,\qquad d\mid b, $$ 则对任意整数 $x,y$,都有 $$ \boxed{d\mid ax+by}. $$ 证明: 由整除的定义,存在整数 ...

    /blog/07_数学/初等数论/初等数论笔记整除最大公因数与同余
  2. 锥线篇(05)二次曲线与中心射影变换 Sep 19, 2026

    先看一道典例。(手动@鸽姬布) 用对合的方式看(这段看不懂忽略即可)点$P$作为对合中心,确立了$A,B$之间的一个对合,记为$\sigma{P}$。$A,B$经过定点$Q$透视后的像$C,D$之间也应该满足对合关系,记这个对合的中心...

    /blog/07_数学/圆曲/锥线篇05二次曲线与中心射影变换
  3. 导数篇(01)怎么巧记对数均值不等式 Sep 19, 2026

    用双曲函数记住一组对数不等式 残留了一点ai味,因为文章大体结构是ai写的,勿在意(。 高中数学极值点偏移问题中经常见一组看起来很难记的不等式: $$ \frac{x^21}{x^2+1} < \frac{2(x1)}{x+1} < ...

    /blog/07_数学/导数篇01怎么巧记对数均值不等式
  4. 权方和不等式 Sep 19, 2026

    由CS不等式,易得 $$ \left( \frac{a^2}{x} + \frac{b^2}{y} \right)(x+y)\geq (a+b)^2 $$ 当$\dfrac{a}{x}=\dfrac{b}{y}$时取等 此时有 $$ ...

    /blog/07_数学/权方和不等式
  5. 锥线篇(00)圆锥曲线子问题分类和解法索引 Sep 12, 2026

    本文未完成,正在施工。预计九月前写完。 高中圆锥曲线的题目经过变形都一般能归化到这些子问题,这篇文章梳理这些子问题,给出典例(不会给具体解法),并给出对应的解法名称与链接。 如果你不知道对合或极点极线并不影响阅读本文,观察例子的普遍形...

    /blog/07_数学/圆曲/锥线篇00圆锥曲线子问题分类和解法索引