I have a broad interest in theoretical computer science. Currently, I am interested in computational complexity, which studies the limitations of efficient computation. Some topics of complexity theory that I find fascinating are circuit complexity, proof complexity, meta-complexity, explicit constructions, and average-case complexity.
At Tsinghua, I was advised by Prof. Ran Duan and worked on graph algorithms. One emphasis of my research was to design shortest-path data structures for graphs in the presence of failures.
(In theoretical computer science, the list of authors are usually sorted in alphabetical order.)
Many Proof Complexity Generators Inside One Demi-Bits Generator, with Xin Li and Yan Zhong
[Slides at SUFE (focused on unprovability of circuit lower bounds)],
[Summary]
Summary: For every demi-bits generator $G: \{0, 1\}^n \to \{0, 1\}^m$ ($m \ge 10n$) and every proof system $\mathcal{P}$, we show that a random subset of its outputs ($G|_I$, $I\gets 2^{[m]}$) forms a proof complexity generator for $\mathcal{P}$ with constant probability. This result is an extremely simple corollary of the Sauer–Shelah lemma. Based on this result, we prove hardness of $\mathsf{NC}^0$-$\mathrm{Avoid}$ and $\mathsf{XOR}$-$\mathrm{RemotePoint}$ based on various hardness assumptions against nondeterministic algorithms.
To appear in IEEE Symposium on Foundations of Computer Science (FOCS) 2026
Near-Maximum Circuit Lower Bounds for Exponential Time with Merlin-Arthur Queries, with Ryan Williams
Summary: We prove a near-maximum ($2^n / n$) circuit lower bound for $\mathsf{E}^{\mathrm{pr}\mathsf{MA}}/_1$. In addition, our hard function can be computed with smart oracle access to $\mathrm{pr}\mathsf{MA}$, i.e., every query is inside the $\mathrm{pr}\mathsf{MA}$ promise.
To appear in IEEE Symposium on Foundations of Computer Science (FOCS) 2026
[ECCC],
[arXiv],
[Slides at Oxford proof complexity workshop (focuses on applications)],
[Summary]
Summary: We investigate the proof complexity of the rank principle, which states that for $n < m$, the product of an $m\times n$ matrix $X$ and an $n\times m$ matrix $Y$ cannot be equal to the $m\times m$ identity matrix. The regime where $n$ is much smaller than $m$ is called the weak rank principle. We prove that the weak rank principle is hard for many proof systems such as Polynomial Calculus with Resolution (PCR) and Sherali-Adams (SA). In fact, we prove that these proof systems cannot prove the rank of any matrix to be small, hence establishing new proof complexity generators. We also explore the connection between weak rank principles and the (un)provability of circuit lower bounds.
In ACM Symposium on Theory of Computing (STOC) 2026
Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds, with Jiawei Li and Yuhao Li
[ECCC],
[arXiv],
[Slides at SJTU (gentle intro)],
[Slides at Oxford proof complexity workshop (slightly more bounded arithmetic)],
[Summary]
Summary: A classic result of Haken shows that any Resolution proof of the pigeonhole principle requires size $> 1.01^n$. We study the "complexity" of proving this lower bound by considering its "refuter" problem: given oracle access to a purported size-$1.01^n$ Resolution proof for the pigeonhole principle, find an illegal derivation in this Resolution proof. We show that this problem is complete for a $\mathsf{TFNP}$ class called $\mathrm{rwPHP}(\mathsf{PLS})$, which is the class corresponding to $\mathsf{NP}$ search problems provably total in $\mathsf{T}^1_2 + \mathrm{dwPHP}(\mathsf{PV})$. Indeed, the containment in $\mathrm{rwPHP}(\mathsf{PLS})$ holds for many Resolution lower bounds proven in the literature and the $\mathrm{rwPHP}(\mathsf{PLS})$-hardness holds for every exponential-size Resolution lower bound that is true.
In ACM Symposium on Theory of Computing (STOC) 2026
Hardness of Range Avoidance and Proof Complexity Generators from Demi-Bits, with Yichuan Wang and Yan Zhong
[ECCC],
[arXiv],
[eprint],
[Independent and concurrent work by Rahul Ilango],
[Slides at Prague Logic Seminar (proof complexity oriented)],
[Slides and video at Princeton Theory Lunch (focused on "cryptography against nondeterministic adversaries")],
[Summary]
Summary: We show that the existence of demi-bits generators (in the sense of Rudich) with suitable stretch implies the range avoidance problem cannot be solved by a nondeterministic algorithm in polynomial time. We extend this result to show that similar assumptions imply proof complexity generators for every proof system, and that these proof complexity generators are pseudo-surjective (in the sense of [Krajíček'04]) in some parameter regimes.
In Innovations in Theoretical Computer Science (ITCS) 2026, Best Student Paper Award
Summary: We present a pseudodeterministic polynomial-time algorithm for constructing primes that works infinitely-often. (That is, although the algorithm is randomized, it outputs a fixed prime with high probability.) As usual(?), the only properties of primes we used are that (1) there are many primes and (2) PRIMES is in P.
In Journal of the ACM; preliminary version in FOCS 2023
[ECCC],
[Twitter],
[Poster at Oxford Computer Science Conference],
[Slides and video at ICMS (focused on proof complexity)],
[Slides at Complexity Meetings],
[Summary]
Summary: In the range avoidance problem, we are given a circuit $C:\{0, 1\}^n\to \{0, 1\}^\ell$ where $\ell > n$, and we want to find a string $y\in\{0, 1\}^\ell$ that is not in the range of $C$. Using Ryan Williams's Algorithmic Method for proving circuit lower bounds, we show that derandomisation of certain data structures would imply an ${\sf FP}^{\sf NP}$ algorithm for solving this problem. As an application of this result, we characterise circuit lower bounds for ${\sf E}^{\sf NP}$ by non-trivial derandomisation algorithms with ${\sf E}^{\sf NP}$ preprocessing.
In IEEE Symposium on Foundations of Computer Science (FOCS) 2022