AI agents · Formal mathematics · Open source
Building agents that turn ideas
into working, verifiable systems.
I’m Yangyang Yu, a Tsinghua University graduate in Information and Computing Sciences. I build AI products and research tools, with a focus on agent memory, multimodal intelligence, and formal mathematics.
从多模态与具身智能研究，到 Agent 产品与开源工具。目前主要构建 Proofweave，探索如何让 AI 参与的数学研究可复现、可验证。
01 / Building
Featured · Formal mathematics
A research agent’s work should be checkable.
A network for personally delegated mathematical research. Private reasoning stays in a local Lean workspace; selected results become signed evidence that others can inspect and reproduce.
Built around scoped agent delegation, isolated Lean replay, and attributable contribution receipts.
Open-source project / AI-assisted DJ tooling
Built a Python HTTP/MIDI sidecar that lets AI agents and MCP clients control Mixxx through its controller mapping API. The bridge handles deck and FX controls, capability discovery, and command acknowledgements while Mixxx owns real-time audio.
Implemented a HELLO/READY handshake, request-linked acknowledgements and state feedback, and a macOS CoreMIDI C helper. Documented a same-value crossfader read/write round trip on Mixxx 2.5.6 on September 1, 2026.
Agent safety / Developer tools
A small, dependency-free toolkit for screening common prompt-injection signals, with advisory agent policies, Python helpers, and regression tests.
Covers direct, encoded, and Unicode-evasion patterns. Heuristic screening complements host-enforced security controls.
AI for mathematics / Research in progress
Connecting complex geometry, topology, and moduli theory through structured tutorials and explicit mathematical interfaces in Lean 4.
Includes selected Mathlib-backed components for charts, families, and descent. Formalization of the full theory remains in progress.
Open-source contribution
Fixed TUI messages being routed to Discord DMs instead of the terminal interface.
02 / Research
My research spans egocentric video understanding, multimodal LLM evaluation, memory-augmented reasoning, efficient fine-tuning, and formal mathematical verification.
A benchmark connecting first-person video understanding to embodied AI through video question answering, hierarchical planning, visual grounding, and reward modeling.
Read the paperStudied when agents should retrieve memory through supervised cold-start training and staged GRPO optimization, with evaluation on FEVER, HotpotQA, and SciWorld.
03 / Experience
Product exploration2025.08 – Present
Exploring intent routing, dual-layer memory, multi-source data fusion, and privacy-aware skin data management. Studying smart-mirror capture and user feedback for personalized skincare decisions.
Co-Founder2023.10 – 2025.10
Built character-based agents and companion robot systems with long-term memory, personalized conversation, and backend deployment. The team secured MiraclePlus seed funding and iterated MVPs through user testing.
Engineering internship2024.07 – 2024.10
Developed multimodal LLM applications and knowledge extraction pipelines for unstructured instructional data, integrating context retrieval and enterprise deployment workflows.
Undergraduate research2023.06 – 2024.06
Worked on context extension, SFT/LoRA, and memory mechanisms. Contributed experiments, data preparation, ablations, and paper writing, including work on VidEgoThink.
Curriculum research2022.08 – 2024.06
Conducted student interviews and analyzed feedback across 10+ CS courses, with a focus on evaluating and improving the Software Engineering course. Contributed course-improvement proposals adopted by the department.
04 / Background
Foundations in mathematics, computer science, and neural networks.
IntelliCompanion, a multimodal desktop companion robot. Led cloud-edge AI architecture and prototype iterations.
Consumer product design, user research, and team collaboration.
Indigenous cultural preservation and environmental sustainability through interviews, workshops, and policy-report writing.
Get in touch
Open to conversations about AI agents, formal mathematics,
multimodal research, and thoughtful AI products.