arXiv subjects
Publications and source records attributed to Yuanjie Ren.
Kolokolnikov conjectured that, among all simple graphs on \(n\) vertices with exactly \(2(n-2)\) edges, the complete bipartite graph maximizes algebraic connectivity. This paper proves the conjecture. The underlying Lean~4 formalization was generated with MerLean and checked by the Lean kernel.
We study the structure of Gibbs states in weakly perturbed interacting fermionic systems. First, for a sparse Hamiltonian $H=H_0+V$ with a quadratic term $H_0$ and a non-quadratic perturbation $V$ of scale $ε$, we show that the Gibbs state $ρ_β$ decomposes into a convex combination of Gaussian states whenever the inverse temperature satisfies $β\le O(\log(1/ε))$. Moreover, we prove that this bound is asymptotically tight by establishing that $β\le Θ(\log(1/ε))$ is necessary for certain sparse Hamiltonians. This general framework applies directly to the weak-coupling (small-$\vert{}U\vert{}$) regime of the Fermi--Hubbard model with hopping $t$ and on-site interaction $U$ on any graph of maximum degree $D$. Complementarily, in the strong-coupling (small-$\vert{}t\vert{}$) regime, we show that the Gibbs state remains convex-Gaussian up to $β\le O\big(\vert{}U\vert{}^{-1}\log(\vert{}U\vert{}/(D\vert{}t\vert{}))\big)$, revealing a mechanism for convex-Gaussianity distinct from the weak-coupling setting.
MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.
The training algorithms for AI systems all introduce far-from-equilibrium dynamical processes, and understanding the irreversibility of these algorithms is a fundamental step towards understanding the learning dynamics of modern AI systems. In this work, we establish a general framework for defining and analyzing the irreversibility of training algorithms. We show that four different ways to characterize the irreversibility of dynamical processes are equivalent to leading order in the step size $η$: numerical backward error $ϕ_{\rm DE}$, time-renormalized correction $ϕ_{\rm TR}$, microscopic time reversal asymmetry $ϕ_{\rm TA}$, and the (regularized) stochastic-thermodynamic entropy production $ϕ_{\rm ST}$. The irreversibility gives rise to a time-reversal-symmetry-breaking emergent force that generically breaks non-isometric continuous reparametrization symmetries, preserves orthogonal symmetries, and leads to a universal preference for those learning trajectories that minimize the entropy production rate.
We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our results demonstrate that agentic autoformalization can scale to frontier research, offering both a practical tool for machine-verified peer review and a scalable engine for mining high-quality synthetic data to train future reasoning models. Our approach can also be generalized to any other rigorous research in mathematics and theoretical physics.
The classification of topological phases of matter is a fundamental challenge in quantum many-body physics, with applications to quantum technology. Recently, this classification has been extended to the setting of Adaptive Finite-Depth Local Unitary (AFDLU) circuits which allow global classical communication. In this setting, the trivial phase is the collection of all topological states that can be prepared via AFDLU. Here, we propose a complete classification of the trivial phase by showing how to prepare all solvable anyon theories that admit a gapped boundary via AFDLU, extending recent results on solvable groups. Our construction includes non-Abelian anyons with irrational quantum dimensions, such as Ising anyons, and more general acyclic anyons. Specifically, we introduce a sequential gauging procedure, with an AFDLU implementation, to produce a string-net ground state in any topological phase described by a solvable anyon theory with gapped boundary. In addition, we introduce a sequential ungauging and regauging procedure, with an AFDLU implementation, to apply string operators of arbitrary length for anyons and symmetry twist defects in solvable anyon theories. We apply our procedure to the quantum double of the group $S_3$ and to several examples that are beyond solvable groups, including the doubled Ising theory, the $\mathbb{Z}_3$ Tambara-Yamagami string-net, and doubled $SU(2)_4$ anyons.
We introduce a graphical calculus, consisting of a set of fermionic tensors with tensor-network equations, which can be used to perform various computations in fermionic many-body physics purely diagrammatically. The indices of our tensors primarily correspond to fermionic modes, but also include qubits and fixed odd-parity states. Our graphical calculus extends the ZX calculus for systems involving qubits. We apply the calculus in order to represent various objects, operations, and computations in physics, including fermionic Gaussian states, the partial trace of Majorana modes, purification protocols, fermionization and bosonization maps, and the construction of fermionic codes.
One potential route toward fault-tolerant universal quantum computation is to use non-Abelian topological codes. In this work, we investigate how to achieve this goal with the quantum double model $\mathcal{D}(S_3)$ -- a specific non-Abelian topological code. By embedding each on-site Hilbert space into a qubit-qutrit pair, we give an explicit construction of the circuits for creating, moving, and locally measuring all non-trivial anyons. We also design a specialized anyon interferometer to remotely measure the total charge of well-separated anyons; this avoids fusion, which would compromise fault tolerance. These protocols enable the implementation of a universal gate set proposed by Cui et al. and active quantum error correction of the circuit-level noise during the computation process. To further reduce the error rate and facilitate error correction, we encode each physical degree of freedom of $\mathcal{D}(S_3)$ into a novel, quantum, error-correcting code, enabling fault-tolerant realization, at the logical level, of all gates in the anyon manipulation circuits. Our proposal offers a promising path to realize robust universal topological quantum computation in the NISQ era.
In this paper, we explore topological quantum computation augmented by subphases and phase transitions. We commence by investigating the anyon tunneling map, denoted as $φ$, between subphases of the quantum double model $\mathcal{D}(G)$ for any arbitrary finite group $G$. Subsequently, we delve into the relationship between $φ$ and the Floquet code, and extend the Abelian Floquet code to encompass non-abelian cases. We conclude by demonstrating how phase transitions in both the temporal and spatial directions can enhance the diversity of topological gates for general topological orders described by modular tensor categories.
We demonstrate that the $p_T$ dependence of the $η/π^0$ ratio is universal within a few percent for high energy $p$+$p$, $p$+A and $d$+A collisions, over a broad range of collision energies. The $η/π^0$ ratio increases with $p_T$ up to 4 to 5 GeV/$c$ where it saturates at a nearly constant value of 0.487$\pm$0.024. Above $p_T = 5$ GeV/$c$ the same constant value is also observed in A+A collisions independent of collision system, energy, and centrality. At lower $p_T$, where accurate $η/π^0$ data is absent for A+A collisions, we estimate possible deviations from the universal behavior, which could arise due to the rapid radial hydrodynamic expansion of the A+A collision system. For A+A collisions at RHIC we find that possible deviations are limited to the $p_T$ range from 0.4 to 3 GeV/$c$, and remain less than 20% for the most central collisions.