Xiaoyu.lean0 of 8 steps

Xiaoyu Li

PhD student · UNSW Computer Science and Engineering

I’m trying to understand myself and the world I find myself in. Mathematics, art, and philosophy are ways I explore it.

This page is a theorem, and you read it by proving it. Press a tactic below, or the hint, and each step opens a part of the site. No mathematics needed; everything is also in a plain list.

What does it mean for AI to help a person?

theorem xiaoyu_li :

∀ v : Visitor, ∃ w : Work, worth_your_time v w := by

-- Your move.

sorryskip the proof

The proof runs on JavaScript, which is off, so here it is finished. Every link is also in the plain list below.

Xiaoyu.lean

Xiaoyu Li

PhD student · UNSW Computer Science and Engineering

I’m trying to understand myself and the world I find myself in. Mathematics, art, and philosophy are ways I explore it.

This page is a theorem, and you read it by proving it. Press a tactic below, or the hint, and each step opens a part of the site. No mathematics needed; everything is also in a plain list.

What does it mean for AI to help a person?

theorem xiaoyu_li :

∀ v : Visitor, ∃ w : Work, worth_your_time v w := by

intro v -- v is you, the visitor

-- The question, in 3 parts:

obtain ⟨purpose, agency, evidence⟩ := the_question

I work on learning theory and explore formal models of goals, assistance, and evidence.

purpose
What should AI help people pursue?
How can people express, revise, and refuse goals? Learning a preference is not permission to act.
Goals · Revision · Authorization
agency
When does help empower rather than replace?
Does assistance increase a person’s ability to understand and act? People should be able to choose how much to delegate and take back control.
Assistance · Capability · Control
evidence
How do we know the help was real?
What observations justify a claim of benefit? When do guarantees survive connections between models, tools, and people?
Identification · Verification · Composition

The research statement

-- Lemmas, each stated in one sentence and proved in a paper.

A Categorical Atlas of Parameter-Efficient Fine-Tuning: Cones, Orbits, and Gauges

Xiaoyu Li, Zhizhou Sha, Chiwun Yang, Dai Shi · Technical report · 2026

PDF Interactive companion

have categorical_atlas_peft : «Hundreds of fine-tuning methods, viewed through one mathematical framework.» := paper

Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit

Xiaoyu Li, Andi Han, Dai Shi, Zheng Gao, Jiaojiao Jiang, Junbin Gao · arXiv:2606.14688 · 2026

have flood_and_harvest : «Discovering unseen valuable mathematics requires infinitely many correct but worthless statements.» := paper

Watermark Forensics for Generative Models: An Information-Theoretic Perspective

Xiaoyu Li, Zheng Gao, Xiaoyan Feng, Jiaojiao Jiang, Yulei Sui, Jiankun Hu · arXiv:2607.13003 · 2026

have watermark_forensics_generative_models : «We quantify the cost of user attribution, payload recovery, and watermark localization.» := paper

When the Canonical Completion Is Wrong: Formalizing and Measuring the Jump in LLMs

Dai Shi, Xiaoyu Li, José Miguel Hernández-Lobato · arXiv:2608.26187 · 2026

have canonical_completion_jump : «We formalize and test whether LLMs can leave a canonical default when constraints demand a different structure.» := paper

Feature Superposition in Neural Networks: From Theory to Practice

Dai Shi, Xiaoyu Li, Andi Han, José Miguel Hernández-Lobato · arXiv:2609.06862 · 2026

have feature_superposition : «We review how neural networks encode more features than dimensions and how to recover them.» := paper

What Pretraining and Midtraining Make Learnable from Rewards?

Chiwun Yang, Xiaoyu Li · arXiv:2609.38446 · 2026

have pretraining_midtraining_rewards : «Task-independent prediction can teach computations that rewards alone leave undetermined.» := paper

-- More: Selected papers · The 2026 archive · Google Scholar

Remark. Not needed for the proof, but written along the way: essays, newest first.

The New Eight-Legged Essays and the Smiling, Proud Wanderer新八股与笑傲江湖October 21, 2026
Why Is the Golden Snitch Worth 150 Points?金色飞贼为什么值150分？October 20, 2026
Can't Learn It? Is It the Concept, or the Teaching?学不会，是概念太难，还是讲法错了？October 17, 2026
Werewolf with a Million Players: 674 Wolves Are Enough一百万人的狼人杀，674 只狼就够了October 17, 2026
Why Don’t We Design Slower Algorithms?October 16, 2026
You Didn't Learn Badly. You Were Taught Too Well.你不是没学好，是被教得太好了October 15, 2026

All 25 essays

-- To show that some w exists: name one (case w), then show it is worth your time (case h).

constructor

Works. Any of these will do for w:

Every work, in one index

case w => exact peft_atlas -- A Categorical Atlas of Parameter-Efficient Fine-Tuning

case h => simp [purpose, agency, evidence]

done

Proof complete.

xiaoyu_li holds for every visitor, including you.

Let’s think about it.

What might we come to understand together, and how shall we spend our brief time here?

xiaoyu.li2[at]unsw[dot]edu[dot]au

Email Google Scholar X · @xiaoyulics

sorry · the proof, skipped

The plain list

Every link on this page, without the proof.

Xiaoyu Li

I’m trying to understand myself and the world I find myself in. Mathematics, art, and philosophy are ways I explore it.

PhD student · UNSW Computer Science and Engineering

The question

What does it mean for AI to help a person?

Purpose What should AI help people pursue?
Agency When does help empower rather than replace?
Evidence How do we know the help was real?
The research statement

Papers

A Categorical Atlas of Parameter-Efficient Fine-Tuning: Cones, Orbits, and Gauges · PDF · Interactive companion · Technical report · 2026
Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit · arXiv:2606.14688 · 2026
Watermark Forensics for Generative Models: An Information-Theoretic Perspective · arXiv:2607.13003 · 2026
When the Canonical Completion Is Wrong: Formalizing and Measuring the Jump in LLMs · arXiv:2608.26187 · 2026
Feature Superposition in Neural Networks: From Theory to Practice · arXiv:2609.06862 · 2026
What Pretraining and Midtraining Make Learnable from Rewards? · arXiv:2609.38446 · 2026
Selected papers
The 2026 archive
Google Scholar

Works

A Categorical Atlas of Parameter-Efficient Fine-Tuning · Interactive atlas
A Categorical Atlas of PEFT: the film · Film · 17 min · narrated
The golden flower · Instrument
The Universe Did Not Include a Progress Bar · Illustrated essay · Six drawings
Essays from Chinese social media · Essays in Chinese and English
Video collections · coming soon
Not yet imagined · open
Every work, in one index

Xiaoyu Li

The plain list

Xiaoyu Li

The question

Papers

Works

Say hello

Other ways in

Essays