arXiv subjects

Weiran Sun

Publications and source records attributed to Weiran Sun.

At least 19 recordsLinked to original sources

arXiv2026

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions, yet existing refactoring works overlook three practical challenges: 1) Lean refactoring is natively multi-objective (proof length, compilation cost, and version compatibility are often in tension); 2) Lean repositories have fragile compatibility, whereas LLM releases are unaware of Lean/Mathlib versions; 3) Training-based pipelines require repeated fine-tuning with each new LLM release, scaling neither with model churn nor with Lean's release cycle. Lean Refactor steers a frozen agentic LLM with retrievals from a curated database of multi-objective refactoring strategies, each densely annotated with metadata such as supported Lean/Mathlib versions and expected compilation-cost reduction. Experiments show over $70\%$ token-level compression on competition benchmarks, over $20\%$ on research repositories, and up to $60\%$ compilation-time reduction, outperforming prior work and Claude Code. Version-filtered retrieval further improves compression on the target Lean version, and refactored miniF2F proofs exhibit stronger zero-shot version transfer to future Lean releases than their unrefactored counterparts.

cs.LO↗

arXiv2025

Uniqueness for the Homogeneous Landau-Coulomb Equation in $L^{3/2}$

We prove the uniqueness of $H$-solutions to the homogeneous Landau-Coulomb equation satisfying $\langle v \rangle^{k_0} f \in C([0, T]; L^{3/2}(\mathbb{R}^3))$ and $\langle v \rangle^{-3/2} \nabla_v ((\langle v \rangle^{k_0} f)^{3/4}) \in L^2((0, T) \times \mathbb{R}^3)$ for any $k_0 \geq 5$. In particular, this shows that the solutions constructed in~\cite{GGL25} are unique. The present work thus completes the global well-posedness theory in the critical space $L^{3/2}(\mathbb{R}^3)$. Our proof is part of a broader effort to use the $\mathcal{M}$-operator technique developed in~\cite{AGS2025, AMSY2020} to establish the uniqueness of rough solutions to nonlinear kinetic equations. When applied to the space-homogeneous case, the $\mathbb{M}$-operator can be taken simply as a Bessel potential operator.

math.AP↗

arXiv2025

Lean Finder: Semantic Search for Mathlib That Understands User Intents

We present Lean Finder, a semantic search engine for Lean and mathlib that understands and aligns with the intents of mathematicians. Progress in formal theorem proving is often hindered by the difficulty of locating relevant theorems and the steep learning curve of the Lean 4 language, making advancement slow and labor-intensive. Existing Lean search engines, though helpful, rely primarily on informalizations (natural language translation of the formal statements), while largely overlooking the mismatch with real-world user queries. In contrast, we propose a user-centered semantic search tailored to the needs of mathematicians. Our approach begins by analyzing and clustering the semantics of public Lean discussions, then fine-tuning text embeddings on synthesized queries that emulate user intents. We further align Lean Finder with mathematicians' preferences using diverse feedback signals, encoding it with a rich awareness of their goals from multiple perspectives. Evaluations on real-world queries, informalized statements, and proof states demonstrate that our Lean Finder achieves over $30\%$ relative improvement compared to previous search engines and GPT-4o. In addition, Lean Finder is compatible with LLM-based theorem provers, bridging retrieval with formal reasoning. Lean Finder is available at: https://leanfinder.github.io

cs.LG↗

arXiv2025

The spectrum of the Steklov-Helmholtz operator

We present a wavenumber-robust strategy for computing Steklov eigenpairs of the Helmholtz operator $-\Delta -\mu^2$. As the wavenumber $\mu \rightarrow \mu_D$ from below (where $\mu_D^2 $ is a Dirichlet- Laplace eigenvalue of multiplicity $\ell$), the lowest $\ell$ Steklov-Helmholtz eigenvalues diverge to $-\infty$. Computationally, the Steklov-Helmholtz eigenvalue problem becomes severely ill-conditioned when $\mu \approx \mu_D$. We first reformulate the problem in terms of a suitably-defined Dirichlet-to-Neumann map. We then use an indirect approach based on a single layer ansatz. The discrete single layer matrix is nearly singular close to exceptional wavenumbers, and we use a reduced singular value decomposition to avoid the consequent ill-conditioning. For smooth domains, convergence of our eigenvalue solver is spectral. We use this method (called the BIO-MOD approach) for shape optimization of scale-invariant Steklov-Helmholtz problems and prove that the disk maximizes the second eigenvalue under appropriate scaling. For curvilinear polygons, we use polynomially-graded meshes rather than uniform meshes. As a proof of concept, we also implemented BIO-MOD using RCIP quadratures (using the ChunkIE implementation). The BIO-MOD approach successfully removes ill-conditioning near exceptional wavenumbers, and very high eigenvalue accuracy (up to 10 digits for polygons, arbitrary precision accuracy for smooth domains) is observed. We deploy our approach to computationally study the spectral geometry of the Steklov-Helmholtz operator, including some questions about spectral asymptotics and spectral optimization.

math.NA↗

arXiv2025

The $\mathcal{M}$-Operator and Uniqueness of Nonlinear Kinetic Equations

We introduce an $\mathcal{M}$-operator approach to establish the uniqueness of continuous or bounded solutions for a broad class of Landau-type nonlinear kinetic equations. The specific $\mathcal{M}$-operator, originally developed in [3], acts as a negative fractional derivative in both spatial and velocity variables and interacts in a controllable manner with the kinetic transport operator. The novelty of this method is that it bypasses the need for bounds on the derivatives of the solution - an assumption typically required in uniqueness arguments for non-cutoff equations. As a result, the method enables working with solutions with low regularity.

math.AP↗

arXiv2025

PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs

While recent AI-for-math has made strides in pure mathematics, areas of applied mathematics, particularly PDEs, remain underexplored despite their significant real-world applications. We present PDE-Controller, a framework that enables large language models (LLMs) to control systems governed by partial differential equations (PDEs). Our approach enables LLMs to transform informal natural language instructions into formal specifications, and then execute reasoning and planning steps to improve the utility of PDE control. We build a holistic solution comprising datasets (both human-written cases and 2 million synthetic samples), math-reasoning models, and novel evaluation metrics, all of which require significant effort. Our PDE-Controller significantly outperforms prompting the latest open source and GPT models in reasoning, autoformalization, and program synthesis, achieving up to a 62% improvement in utility gain for PDE control. By bridging the gap between language generation and PDE systems, we demonstrate the potential of LLMs in addressing complex scientific and engineering challenges. We release all data, model checkpoints, and code at https://pde-controller.github.io/.

cs.LG↗

arXiv2025

Crossover from ballistic transport to normal diffusion: a kinetic view

The crossover between dispersion patterns has been frequently observed in various systems. Inspired by the pathway-based kinetic model for E. coli chemotaxis that accounts for the intracellular adaptation process and noise, we propose a kinetic model that can exhibit a crossover from ballistic transport to normal diffusion at the population level. At the particle level, this framework aligns with a stochastic individual-based model. Using numerical simulations and rigorous asymptotic analysis, we demonstrate this crossover both analytically and computationally. Notably, under suitable scaling, the model reveals two distinct limits in which the macroscopic densities exhibit either ballistic transport or normal diffusion.

math.AP↗

arXiv2024

Pickleball Flight Dynamics

This paper considers the flight dynamics of the ball in the sport of pickleball. Various simplifications are introduced according to the features of the game. These simplifications and some approximations enable straightforward coding to study aspects of the game such as the trajectory of the ball and its velocity. In turn, strategic questions may be addressed that have not been previously considered. In particular, our primary research question involves the preference between playing with the wind versus against the wind. It is demonstrated that playing against the wind is often preferable than playing with the wind.

physics.soc-ph↗

arXiv2024

$L^p$-norms for the homogeneous non-cutoff Boltzmann equation with soft potentials

We establish a priori estimates showing the propagation and generation of $L^p$-norms for solutions to the non-cutoff spatially homogeneous Boltzmann equation with soft potentials. The singularity of the collision kernel is key to generate regularization and inhomogeneity in the energy estimates of the $L^p$-norms. Our result extends \cite{Alo19} from the hard potential cases to the soft ones.

math.AP↗

arXiv2024

Reconstruction of the Doping Profile in Vlasov-Poisson

We study the inverse problem of recovering the doping profile in the stationary Vlasov-Poisson equation, given the knowledge of the incoming and outgoing measurements at the boundary of the domain. This problem arises from identifying impurities in the semiconductor manufacturing. Our result states that, under suitable assumptions, the doping profile can be uniquely determined through an asymptotic formula of the electric field that it generates.

math.AP↗

arXiv2022

Uniform error estimate of an asymptotic preserving scheme for the L\'{e}vy-Fokker-Planck equation

We establish a uniform-in-scaling error estimate for the asymptotic preserving scheme proposed in \cite{XW21} for the L\'evy-Fokker-Planck (LFP) equation. The main difficulties stem from not only the interplay between the scaling and numerical parameters but also the slow decay of the tail of the equilibrium state. We tackle these problems by separating the parameter domain according to the relative size of the scaling $\epsilon$: in the regime where $\epsilon$ is large, we design a weighted norm to mitigate the issue caused by the fat tail, while in the regime where $\epsilon$ is small, we prove a strong convergence of LFP towards its fractional diffusion limit with an explicit convergence rate. This method extends the traditional AP estimates to cases where uniform bounds are unavailable. Our result applies to any dimension and to the whole span of the fractional power.

math.NA↗

arXiv2022

Second-order diffusion limit for the phonon transport equation-asymptotics and numerics

We investigate the numerical implementation of the limiting equation for the phonon transport equation in the small Knudsen number regime. The main contribution is that we derive the limiting equation that achieves the second order convergence, and provide a numerical recipe for computing the Robin coefficients. These coefficients are obtained by solving an auxiliary half-space equation. Numerically the half-space equation is solved by a spectral method that relies on the even-odd decomposition to eliminate corner-point singularity. Numerical evidences will be presented to justify the second order asymptotic convergence rate.

math.NA↗

arXiv2021

Unique Reconstruction of the Heat-Reflection Indices at Solid Interfaces

We show the unique reconstruction of the heat-reflection coefficients in a phonon transport equation. This is a mathematical model used to characterize the dynamics of heat-conducting phonons in multiple layers of media, commonly composed of metals and silicon. In experiments, the heat-reflection indices are inferred by measuring the temperature at the surface of the exterior metal after applying heat sources. In this article, we rigorously justify the unique reconstruction of these indices by using such procedures.

math.AP↗

arXiv2019

Mathematical Modelling and Analysis of Fractional Diffusion Induced by Intracellular Noise

In this paper we use an individual-based model and its associated kinetic equation to study the generation of long jumps in the motion of E. coli. These models relate the run-and-tumble process to the intracellular reaction where the intrinsic noise plays a central role. Compared with the previous work in [13] in which the parametric assumptions are mainly for mathematical convenience and not well-suited for either numerical simulation or comparison with experimental results, our current paper make use of biologically meaningful pathways and tumbling kernels. Moreover, using the individual-based model we can now perform numerical simulations. Power-law decay of the run length, which corresponds to Levy-type motions, are observed in our numerical results. The particular decay rate agrees quantitatively with the analytical result. We also rigorously recover the fractional diffusion equation as the limit of the kinetic model.

math.AP↗

arXiv2019

Applications of Kinetic Tools to Inverse Transport Problems

We show that the inverse problems for a class of kinetic equations can be solved by classical tools in PDE analysis including energy estimates and the celebrated averaging lemma. Using these tools, we give a unified framework for the reconstruction of the absorption coefficient for transport equations in the subcritical and critical regimes. Moreover, we apply this framework to obtain, to the best of our knowledge, the first result in a nonlinear setting. We also extend the result of recovering the scattering coefficient in [14] from 3D to 2D convex domains.

math.AP↗

arXiv2019

Multiple asymptotics of Kinetic Equations with Internal States

The run and tumble process is well established in order to describe the movement of bacteria in response to a chemical stimulus. However the relation between the tumbling rate and the internal state of bacteria is poorly understood. The present study aims at deriving models at the macroscopic scale from assumptions on the microscopic scales. In particular we are interested in comparisons between the stiffness of the response and the adaptation time. Depending on the asymptotics chosen both the standard Keller-Segel equation and the flux-limited Keller-Segel (FLKS) equation can appear. An interesting mathematical issue arises with a new type of equilibrium equation leading to solution with singularities.

math.AP↗

arXiv2019

Uniqueness of Solutions to a Gas-Disk Interaction System

In this paper we give an elementary proof of uniqueness of solutions to a gas-disk interaction system with diffusive boundary condition. Existence of near-equilibrium solutions for this type of systems with various boundary conditions has been extensively studied in [1-8, 10]. However, the uniqueness has been an open problem, even for solutions near equilibrium. Our work gives the first rigorous proof of the uniqueness among solutions that are only required to be locally Lipschitz; in particular, it holds for solutions far from equilibrium states.

math.AP↗

arXiv2019

Non-Cutoff Boltzmann Equation with Polynomial Decay Perturbation

The Boltzmann equation without an angular cutoff is considered when the initial data is a small perturbation of a global Maxwellian with an algebraic decay in the velocity variable. A well-posedness theory in the perturbative framework is obtained for both mild and strong angular singularities by combining three ingredients: the moment propagation, the spectral gap of the linearized operator, and the regularizing effect of the linearized operator when the initial data is in a Sobolev space with a negative index. A carefully designed pseudo-differential operator plays an central role in capturing the regularizing effect. Moreover, some intrinsic symmetry with respect to the collision operator and an intrinsic functional in the coercivity estimate are essentially used in the commutator estimates for the collision operator with velocity weights.

math.AP↗