6 papers
Non-explosion principles for branched rough differential equations with unbounded coefficients
Kexing Ying
Expanding upon the work of arXiv:2502.08799, we provide a non-explosion criterion for branched rough differential equations (bRDEs) where we continue to allow for the drift and the…
Central limit theorem for the Allen-Cahn equation with supercritical random initial conditions
Colin Piernot, Kexing Ying
We study the large-scale behavior of solutions to the Allen-Cahn reaction-diffusion equation with Gaussian initial data. We consider the case of short-range dependence in the assoc…
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
Nikil Ravi, Kexing Ying, Vasilii Nesterov +5
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a n…
Fluctuations from a random fractional averaging limit
Xue-Mei Li, Colin Piernot, Szymon Sobczak +1
We consider a system of multiscale stochastic differential equations whose slow component is drivenby a fractional Brownian motion with Hurst parameter H greater than 1/2. Under er…
Strong completeness of SDEs and non-explosion for RDEs with coefficients having unbounded derivatives
Xue-Mei Li, Kexing Ying
We establish a non-explosion result for rough differential equations (RDEs) in which the noise and drift coefficients, together with their derivatives, may grow unboundedly at infi…
A Formalization of Doob's Martingale Convergence Theorems in mathlib
Kexing Ying, Rémy Degenne
We present the formalization of Doob's martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingal…