Publications and Preprints

Double click "Abstract" below to display the abstract.

• J. K. Miller. A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game. (2026). Abstract. ArXiv Link.
  We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game. The objective is to turn a LaTeX document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone. Reuse is a second check, by a definition we introduce: whether the development yields a self-contained layer of general mathematics the wider library could absorb. The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route -- existence, uniqueness, the stability estimate and mean-field limit, and a short-window superposition principle (weak solutions are Lagrangian). The human's role was to direct, not to write proofs: to scope the definitions, steer the decompositions, and triage the library's gaps; the AI agent executed. The formalization certifies the proof of each statement as written; whether the written statement is the intended theorem stays the mathematician's judgment. The optimal-transport machinery that fell out of the build (in particular, properties of the Wasserstein-1 metric and the Kantorovich-Rubinstein duality theorem) separates into a self-contained layer that compiles against Mathlib alone: about a sixth of the development (49 of 299 declarations), behind a 22-declaration interface with no reverse dependency. The headline theorems ran in about a week, the full development in about a month. We report the quantitative claims as observations of one game, not as general laws. The game's rules name no particular system, so the methodological framing is meant to outlast the tools of any one run.
• E. Cárdenas, J. K. Miller, D. Mitrouskas, N. Pavlović. On the stability-instability transition in large Bose-Fermi mixtures. (2025). Abstract. ArXiv Link.
  We study the low-energy spectrum of large Bose-Fermi mixtures. In the chosen scaling, the fermions induce an effective attraction among the bosons, which competes with their intrinsic repulsive interaction. Our main result demonstrates the convergence of the eigenvalues towards those of an effective Bose Hamiltonian. For short-range potentials, we apply this result to derive a stability-instability transition in the bosonic subsystem, driven by the Bose-Fermi coupling strength g. For small |g|, the bosons form a stable Bose-Einstein condensate with the energy per particle uniformly bounded from below. For large |g|, the energy per particle is no longer uniformly bounded from below, signalling the collapse of the condensate.
• J. K. Miller. On deriving kinetic equations and their structure from classical many-body dynamics. PhD Thesis, (2024). Abstract. Link.
  This dissertation is broken into two parts. In the first part, we rigorously derive a Boltzmann equation for mixtures from the many body dynamics of two types of hard sphere gases. We construct the dynamics, introduce the concept of a two parameter BBGKY hierarchy, and as a corollary of the derivation prove Boltzmann's propagation of chaos for a mixtures of gases. In the second part, we consider the Vlasov equation viewed as an infinite-dimensional Hamiltonian system. We provide a rigorous derivation of this Hamiltonian structure, which includes both the Hamiltonian functional and Poisson bracket, directly from the many-body problem.
• I. Ampatzoglou, J. K. Miller, N. Pavlović, M. Tasković. Inhomogeneous wave kinetic equation and its hierarchy in polynomially weighted $L^\infty$ spaces. Communications in Partial Differential Equations, 50(6), 723-765. (2025). Abstract. Article Link. ArXiv Link.
  Inspired by ideas stemming from the analysis of the Boltzmann equation, in this paper we expand well-posedness theory of the spatially inhomogeneous 4-wave kinetic equation, and also analyze an infinite hierarchy of PDE associated with this nonlinear equation. More precisely, we show global in time well-posedness of the spatially inhomogeneous 4-wave kinetic equation for polynomially decaying initial data. For the associated infinite hierarchy, we construct global in time solutions using the solutions of the wave kinetic equation and the Hewitt-Savage theorem. Uniqueness of these solutions is proved by using a combinatorial board game argument tailored to this context, which allows us to control the factorial growth of the Dyson series.
• I. Ampatzoglou, J. K. Miller, N. Pavlović, M. Tasković. On the global in time existence and uniqueness of solutions to the Boltzmann hierarchy. Journal of Functional Analysis, Volume 289, Issue 9, 1 November 2025. Abstract. Article Link. ArXiv Link.
  In this paper we establish the global in time existence and uniqueness of solutions to the Boltzmann hierarchy, a hierarchy of equations instrumental for the rigorous derivation of the Boltzmann equation from many particles. Inspired by available $L^\infty$-based a-priori estimate for solutions to the Boltzmann equation, we develop the polynomially weighted $L^\infty$ a-priori bounds for solutions to the Boltzmann hierarchy and handle the factorial growth of the number of terms in the Dyson's series by reorganizing the sum through a combinatorial technique known as the Klainerman-Machedon board game argument. This paper is the first work that exploits such a combinatorial technique in conjunction with an $L^\infty$-based estimate to prove uniqueness of the mild solutions to the Boltzmann hierarchy. Our proof of existence of global in time mild solutions to the Boltzmann hierarchy for admissible initial data is constructive and it employs known global in time solutions to the Boltzmann equation via a Hewitt-Savage type theorem.
• E. Cárdenas, J. K. Miller, N. Pavlović. On the Effective Dynamics of Bose-Fermi Mixtures. Ars Inveniendi Analytica. (2025). Abstract. Article Link. ArXiv Link.
  In this work, we describe the dynamics of a Bose-Einstein condensate interacting with a degenerate Fermi gas, at zero temperature. First, we analyze the mean-field approximation of the many-body Schrödinger dynamics and prove emergence of a coupled Hartree-type system of equations. We obtain rigorous error control that yields a non-trivial scaling window in which the approximation is meaningful. Second, starting from this Hartree system, we identify a novel scaling regime in which the fermion distribution behaves semi-clasically, but the boson field remains quantum-mechanical; this is one of the main contributions of the present article. In this regime, the bosons are much lighter and more numerous than the fermions. We then prove convergence to a coupled Vlasov-Hartee system of equations with an explicit convergence rate.
• J. K. Miller, A. R. Nahmod, N. Pavlović, M. Rosenzweig, G. Staffilani. A Rigorous Derivation of the Hamiltonian Structure for the Vlasov Equation. Forum of Mathematics, Sigma, 11, e77. (2023). Abstract. Article Link. ArXiv Link
  We consider the Vlasov equation in any spatial dimension, which has long been known to be an infinite-dimensional Hamiltonian system whose bracket structure is of Lie-Poisson type. In parallel, it is classical that the Vlasov equation is a mean-field limit for a pairwise interacting Newtonian system. Motivated by this knowledge, we provide a rigorous derivation of the Hamiltonian structure of the Vlasov equation, both the Hamiltonian functional and Poisson bracket, directly from the many-body problem. One may view this work as a classical counterpart to arXiv:1908.03847, which provided a rigorous derivation of the Hamiltonian structure of the cubic nonlinear Schrödinger equation from the many-body problem for interacting bosons in a certain infinite particle number limit, the first result of its kind. In particular, our work settles a question of Marsden, Morrison, and Weinstein on providing a "statistical basis" for the bracket structure of the Vlasov equation.
• I. Ampatzoglou, J. K. Miller, N. Pavlović. A Rigorous Derivation of a Boltzmann System for a Mixture of Hard-Sphere Gases. SIAM Journal on Mathematical Analysis, Vol. 54, Iss. 2. (2022). Abstract. Article Link. ArXiv Link.
  In this paper, we rigorously derive a Boltzmann equation for mixtures from the many body dynamics of two types of hard sphere gases. We prove that the microscopic dynamics of two gases with different masses and diameters is well defined, and introduce the concept of a two parameter BBGKY hierarchy to handle the non-symmetric interaction of these gases. As a corollary of the derivation, we prove Boltzmann's propagation of chaos assumption for the case of a mixtures of gases.
• J. Lyons, J. K. Miller. The Derivative of a Solution to a Second Order Parameter Dependent Boundary Value Problem with a Non-Local Integral Boundary Condition. Journal of Mathematical and Statistical Science, Vol. 2015, Iss. 2. (2015). Abstract. Article Link
  We discuss derivatives of the solution of the second order parameter dependent boundary value problem with an integral boundary condition y”=f(x,y,y′,λ),y(x1)=y1,y(x2)+∫dcry(x)dx=y2 y”=f(x,y,y′,λ),y(x1)=y1,y(x2)+∫cdry(x)dx=y2 and its relationship to a second order nonhomogeneous differential equation which corresponds to the traditional variational equation. Specifically, we show that given a solution y(x) of the boundary value problem, the derivative of the solution with respect to the parameter λ is itself a solution to the aforementioned nonhomogeneous equation with interesting boundary conditions.