个人主页

我是王延泽，即将毕业的数学博士生。

在中国科学院大学数学专业读博，主要研究方向为双有理几何，具体涉及极小模型纲领与叶层化理论。研究成果详见论文列表，另有数学笔记。
日常在 Arch Linux + Niri/dwm + Neovim 下开发。正在学习和实践大模型训练、智能体搭建、数学形式化证明等，详情见项目列表和开发文档。
除此之外会日常写一些博文，更多内容在Memex站点。

可以通过关于页面了解，或下载简历。

经历

教育经历

  • 理学博士（在读） — 中国科学院大学，预计 2027 年毕业
  • 理学硕士 — 中国科学院大学，2024 年
  • 理学学士 — 北京航空航天大学，2020 年

教学

  • 助教，北京航空航天大学（本科期间）：线性代数、代数几何

荣誉奖励

  • 美国大学生数学建模竞赛（MCM/ICM） — 一等奖（Meritorious Winner，两次）
  • 北京航空航天大学华罗庚奖学金（两次）

学术报告

  • 2026 年 — 报告人，代数可积与三维叶层化的 Sarkisov 纲领，西交利物浦大学

项目

更多内容见项目文档站点和计算机科学学习记录。

  1. micro-agent

    面向本地开发任务的轻量软件工程智能体，以 Bash 工具循环为核心，支持 ask、auto、yolo 三种自主模式、交互式终端与 JSONL 编排接口；提供可动态追加和重读的 system prompt、AGENTS.md 自动发现、Skills 管理及会话恢复，便于定制项目规则并扩展 subagent 工作流。

  2. DiAgent

    基于 jujutsu 探索以文本变更为中心的智能体工作方式：将任务整理为可组合的原子对话历史，以稳定文本和 diff 组织模型上下文，并研究如何借助版本分支、历史重组与分布式 subagent 支持并行探索和协作。

  3. ARnDlm

    以统一的模型配置、中文语料、tokenizer 与评估流程，系统比较自回归语言模型和扩散语言模型；涵盖模型实现、训练起点、阶段顺序、基础模型规模与 A2D 实现五组对照，并提供可复查的训练与数值校验流程。

  4. lean-toric

    使用 Lean 4 与 mathlib 逐步形式化环面几何，将格、锥与扇等组合基础连接到分裂环面射影丛、轨道分层、扇细分、爆破和初等变换；以经典例子校验数学约定，并建立可编译、可复用的机器检查证明。

  5. MiniMind

    基于开源 MiniMind 开展小型语言模型的代码研究与训练复现，实践从中文数据准备、模型结构与预训练，到监督微调、LoRA、偏好优化、强化学习、工具调用和蒸馏等流程；相关语料与 tokenizer 也为 ARnDlm 的自回归和扩散模型对照实验提供基础。

论文