2025.01 - 2025.03
形式化验证数据标注
- 使用 Lean 证明助手对数学竞赛题目进行定理形式化与验证。
Curriculum Vitae
千秋
独立开发者 · 图形系统 · 形式化验证
个人总结
- 独立开发者，长期关注图形学、Rust、Lisp、开发工具与编程语言。
- 使用 Rust + WebGPU 从零实现类 Minecraft 体素游戏引擎。提供了具有一致性的API接口。使用了多种优化算法和技巧。
- 基于 Lean 对 IMO 数学题进行形式化与验证，熟悉函数式编程和定理证明形式化。
- 完成多个毕业设计，大作业等端到端构建，负责从需求沟通到交付的全流程。
- 建立了 Vibe Coding 与人工审核相结合的工作流，完成了一系列工具的开发。
工作经历
2025.03 - 至今
自由职业 / 接单开发
- 独立开发表格处理、图像识别、数据清洗和任务自动化脚本。
- 负责需求澄清、方案设计、代码实现、交付与后续沟通。
主要项目
Blockworld
类 Minecraft 游戏引擎，致力于源码级兼容 Minecraft 客户端/服务端。
- 使用内存池、RAII、静态Lazy加载等多种混合方式进行高性能内存管理。
- 实现视锥剔除，相邻面剔除等渲染优化算法。
- 使用 Channel/mpsc 在多个线程上并发生成游戏地图，提升地形生成速度。
Moonbite
2024年 MoonBit 全球编程创新挑战赛比赛项目
- 在项目中探索 Hindley-Milner 风格类型系统和语言实现中的工程取舍。
- 实现 tokenizer/lexer/static single-assignment form IR/CPS IR 多级 pass。
Bee Agent
基于 Anthropic Go SDK 实现的编码 Agent，包含终端会话、权限控制、技能、记忆和可视化 Agent/Workflow 配置。
- 实现 Bubble Tea TUI、会话持久化与恢复、模式切换和工具权限确认流程。
- 构建 Agent Builder 与 Workflow DAG，支持 typed node graph、blueprint、dry-run、compiled plan 和 run history。
- 实现记忆、后台任务、cron 调度、subagent、消息平台适配、Telegram 接入和 CoC 跑团工具等模块。
技术写作与笔记
长期在知乎等网站上发布技术相关内容。
- 涵盖CG/数学/函数式编程等方面