2025.01 - 2025.03
Formal Verification Developer
- Formalized and verified competition mathematics problems with the Lean theorem prover.
Curriculum Vitae
千秋 / BreakingLead
Independent Developer · Graphics Systems · Formal Verification
I build tools where theory and implementation meet: graphics engines, compiler experiments, functional programming, theorem proving, and practical automation. I am looking for open source, developer tooling, formal methods, graphics, or general development work in Shanghai or remote teams.
Summary
- 54 public GitHub repositories, with work centered on graphics, Rust, Lisp, and developer tooling.
- Built a Rust + WebGPU voxel engine with ECS architecture and source-level Minecraft mod compatibility as a design goal.
- Used Lean to formalize and verify IMO-style mathematics, combining proof engineering with functional programming.
- Delivered freelance Python automation and data-processing tools from requirements discussion through handoff.
Experience
2025.03 - Present
Freelance Developer
- Built scripts and tools for spreadsheet processing, image recognition, data cleanup, and task automation.
- Handled requirements clarification, technical planning, implementation, and delivery independently.
Selected Projects
Blockworld
A Minecraft-like voxel game implementation with a Rust rendering stack, WebGPU pipeline, and entity-component architecture.
- Designed the core engine architecture, entity management, and rendering pipeline.
- Explored high-performance per-voxel rendering and mod-compatibility-oriented architecture.
Moonbite
A mini MoonBit compiler experiment covering parsing, type checking, and code-generation ideas.
- Built compiler components while exploring Hindley-Milner style typing and language implementation tradeoffs.
Bee Agent
A Go-based coding agent built around the Anthropic Go SDK, with terminal sessions, permission control, skills, memory, and visual agent/workflow configuration.
- Implemented a Bubble Tea TUI with session persistence, resume flows, mode switching, and tool-permission confirmations.
- Built Agent Builder and workflow tooling for typed node graphs, reusable blueprints, dry-runs, compiled plans, and run history.
- Added modules for memory, background jobs, cron scheduling, subagents, messaging adapters, Telegram integration, and CoC tabletop tools.
Technical Writing
Maintains notes and essays on graphics libraries, C/C++ linkage, CPS, ASTs, Zig, Rust, math, and language learning.
- Publishes imported notes and Zhihu articles as a browsable file-style blog archive.
Skills
Languages
Systems & Graphics
Web & Backend
Theory
Education
Northwestern Polytechnical University Affiliated High School
Public Profile
GitHub: BreakingLead
Public profile and repository list show active work across graphics, compiler experiments, dotfiles, Lean study, and programming-language learning.