Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

This paper reports that the full mean-field derivation of the Vlasov equation — existence, uniqueness, stability, mean-field limit, and a short-window superposition principle — is now machine-checked in the Lean proof assistant, with the ta

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 07:43 UTC pith:LUJCK3KG

load-bearing objection A genuinely useful case study of AI-directed Lean formalization, with a clean reusable Wasserstein layer; the mean-field-limit corollary is honestly conditional, so the abstract oversells by a notch. the 3 major comments →

arxiv 2607.08986 v2 pith:LUJCK3KG submitted 2026-07-09 cs.AI cs.LOmath-phmath.APmath.MP

A Formalization of the Mean-Field Derivation of the Vlasov Equation

Joseph K. Miller This is my paper
classification cs.AI cs.LOmath-phmath.APmath.MP MSC 35Q8349Q2268V20
keywords Vlasov equationmean-field limitLean formalizationWasserstein-1 metricKantorovich-Rubinstein dualitysuperposition principleAI-assisted theorem provingformal proof
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper's central assertion is that a complete, axiom-clean formalization of the classical mean-field derivation of the Vlasov equation exists in the Lean proof assistant. A mathematician directed an AI system to turn a LaTeX paper into Lean, with a formal win condition: the development compiles, contains no 'sorry', and the target theorems' axiom footprint is exactly the foundational axioms. The case study covers global well-posedness, the stability estimate, the mean-field limit, and a short-window superposition principle, and the 49-declaration optimal-transport layer compiles against the standard library alone behind a 22-declaration interface. Every formal statement in the appendix is machine-checked; what remains a human judgment is whether those statements are the intended theorems.

Core claim

The author claims to have won the formalization game on this target: the development compiles, no sorry remains, and #print axioms returns exactly [propext, Classical.choice, Quot.sound]. The headline theorems — vlasovWellPosedness, the stability theorem, the mean-field limit, and the superposition principle — are all present, and the proof of each statement as written is certified by Lean. The mean-field limit corollary, however, takes the stability estimate for every empirical curve as an explicit hypothesis; the paper asserts in prose that this estimate holds because each empirical curve is a Lagrangian solution with finite first moments, but no Lean theorem discharging that property is r

What carries the argument

The Wasserstein-1 metric in its dual (Lipschitz-supremum) and primal (coupling-infimum) forms, bridged by a formalized Kantorovich–Rubinstein duality. The stability argument is carried in the coupling formulation, requiring only epsilon-optimal couplings, which avoids an attainment theorem. The superposition principle hinges on a regularity class AssW2 (the potential's gradient is C1), whose role is to make the characteristic flow C1 in initial data so the transported test function is admissible. Exact tiling of short windows removes smallness constraints that would falsely restrict the Lipschitz constant.

Load-bearing premise

The load-bearing claim that the empirical measure curve of N Newtonian particles is a Lagrangian Vlasov solution with finite first moments is asserted in prose but is not itself a machine-checked theorem; the formalized mean-field limit takes the stability estimate for that curve as an explicit hypothesis.

What would settle it

Inspect the public Lean development: check whether any theorem in the reachable proof graph discharges the stability estimate for the empirical measure curve for all N. If no such theorem exists, then the mean-field limit as formalized is conditional on an unformalized assumption, and the abstract's 'mean-field limit' overstates what Lean certifies.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The target theorems for global well-posedness, stability, and the short-window superposition principle are machine-checked; any reader can re-run the build and verify the axiom footprint.
  • The extracted optimal-transport layer — Wasserstein-1 in both faces, Kantorovich–Rubinstein duality, the coupling-gluing triangle inequality, and a finite Kantorovich duality — is a standalone package that could be absorbed into the standard library.
  • The formalization forces the exact regularity needed: the superposition principle requires one extra degree beyond the base assumption, and this becomes visible as a typeclass field rather than a vague prose condition.
  • As formalized, the mean-field limit is conditional on the stability estimate holding for each empirical curve; the paper argues this follows from the empirical curve being a Lagrangian solution, but the Lean statement carries it as an explicit hypothesis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A natural next formalization step is to prove in Lean that the Newtonian empirical measure curve is a Lagrangian Vlasov solution with finite first moments; discharging that would make the mean-field limit unconditional and close the gap between the abstract's claim and the formal statement.
  • The formalization-game protocol — lock the API early, steer decompositions mid-game, triage library gaps late — may transfer to other PDE formalizations as a reusable strategy, independent of the specific AI tool used.
  • The layer's isolation checks (interface width, zero reverse edges, standalone compilation) offer a template for measuring reusability of formalized mathematics, moving beyond size fractions to structural pass/fail criteria.
  • Since chaining short windows to arbitrary T is not formalized for the superposition bridge, a testable extension is to formalize that chaining and extend the short-window theorem globally.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper reports an AI-assisted Lean 4 formalization of Dobrushin's mean-field derivation of the Vlasov equation. It frames the activity as a 'formalization game' with a win condition: the development compiles, contains no sorry, and the target theorems have axiom footprint exactly [propext, Classical.choice, Quot.sound]. It reports formalized global well-posedness, Dobrushin stability, a mean-field limit corollary, and a short-window superposition principle, along with a 49-declaration self-contained optimal-transport layer behind a 22-declaration interface. The paper is also a methodology case study, with quantitative claims about the sorry front, commit record, and standing-instruction file.

Significance. If the repository is as described, this is a substantial and reproducible AI-assisted formalization of a dynamical PDE result, and the explicit win-condition/self-contained-layer checks are a constructive contribution to formalization practice. The paper's transparency about the vacuous test-class episode and the deferred Wasserstein-completeness fact is a strength, as is the public commit record. The main mathematical content is classical, but the formal artifact is genuine. The mean-field-limit caveat detailed below tempers the headline claim without undermining the methodological contribution.

major comments (3)
  1. [Appendix A, Corollary 1.6 (`meanFieldLimit`)] The central certified claim is conditional. The theorem has an explicit hypothesis `hDobrushin : ∀ N, DobrushinStabilityEstimate ...`, and no reported Lean declaration discharges it for the empirical curve. Section 3.3 concedes this: 'the Lean takes it as an explicit hypothesis rather than re-deriving it.' Because propositional hypotheses are not axioms, `#print axioms meanFieldLimit` can return exactly [propext, Classical.choice, Quot.sound] even though the theorem is an implication from an unproved premise. The abstract's 'complete ... mean-field limit' therefore overstates what Lean certifies. Please either formalize the missing instance (empirical curve is Lagrangian, finite first moments, uniform C, then instantiate `dobrushin`) or consistently present the result as a conditional mean-field limit and list this as a limitation.
  2. [Section 3.1 and Appendix A, `IsVlasovSolution`] The weak-solution test class as printed is internally inconsistent. The prose says the top exponent in `ContDiff ℝ ⊤` means real-analytic, causing the test class to collapse, and that the fix was `ContDiff ℝ (⊤ : ℕ∞)`. But the displayed definition in both the body and Appendix A uses exactly `ContDiff ℝ (⊤ : ℕ∞)`. If `⊤` in the pinned Mathlib denotes real-analytic, the corrected predicate is still vacuous and every theorem quantifying over `IsVlasovSolution` becomes trivial; if it denotes C∞, the explanation is wrong. Please state the precise meaning of `⊤` in Mathlib v4.29.1 and confirm by `#check` that nonzero compactly supported functions satisfy the displayed hypothesis.
  3. [Section 3.3, Theorem 1.5 (`dobrushin`)] The formal `dobrushin` statement returns only existence of a constant `C`, not the explicit rate `C = 2 max(1,L)` claimed in the prose and used to justify uniformity in N for `meanFieldLimit`. The sentence 'Theorem 1.5 supplies the assumed estimate' is not supported by the displayed formal statement unless an additional formal theorem with an explicit, N-independent C is present. Please report that formal statement, or soften the prose to distinguish the informal rate calculation from the certified existential theorem.
minor comments (4)
  1. [Section 1.3, `vlasovWellPosedness_uniqueness`] The displayed uniqueness theorem has hypothesis `hL_pos : (0:ℝ) < L`, while the prose says the degenerate L = 0 case is explicit and uniqueness holds at every L. Please display the L = 0 statement or point to its declaration in the repository.
  2. [Section 4.4, deferred completeness fact] The deferred Polish-space Wasserstein completeness fact is said to lie 'off the path of the certified target theorems.' A sentence naming the declaration(s) that would have consumed it, or explaining why the fixed-point construction avoids it, would help a reader who expects completeness to be needed for Banach-fixed-point arguments in W1.
  3. [General] For a formalization paper, please include a pinned repository commit hash or a versioned snapshot in the manuscript, so that the claimed #print axioms results can be re-run against the exact artifact described.
  4. [Throughout] There are several typographical ligature artifacts (e.g., 'difficulty', 'A vigad') that should be cleaned in the final version.

Circularity Check

0 steps flagged

No significant circularity: the formalization is self-contained, and the only notable gap is an explicitly stated conditional hypothesis, not a circular derivation.

full rationale

The derivation chain in this paper does not reduce any target result to its own inputs. The central mathematical claims — existence, uniqueness, Dobrushin stability, the mean-field limit, and the short-window superposition principle — are stated as Lean theorems and proved from library primitives and explicitly stated hypotheses. The paper freely discloses the one place where the formal statement is conditional: `meanFieldLimit` (Appendix A) carries `hDobrushin : ∀ N, DobrushinStabilityEstimate (empiricalMeasureCurve N (X N) (V N)) f C` as an explicit hypothesis, and Section 3.3 says "the Lean takes it as an explicit hypothesis rather than re-deriving it." This is not circularity: the stability estimate is a stronger, independent input from which the limit follows; it is not defined in terms of the limit, nor is the limit fitted or renamed as that hypothesis. The clean axiom footprint is compatible with this because propositional hypotheses are not axioms; this affects the strength of the claim that the mean-field limit is fully certified, a concern the paper itself acknowledges, but it does not make the proof circular. The self-contained-layer check Q4 is admittedly "holds by construction," but the paper says so explicitly and does not use it as independent evidence for the mathematics. The only self-citation, [36], appears in the outlook as future work and is not load-bearing. No step in the paper equates a prediction with a fitted parameter or imports a uniqueness theorem from the authors' prior work as a forced choice. The formalization is therefore honestly conditional where conditional and not circular.

Axiom & Free-Parameter Ledger

0 free parameters · 7 axioms · 0 invented entities

The paper's mathematical claims are classical; the ledger records the regularity, window, continuity, and library premises the formalized statements quantify over, plus the one undischarged hypothesis in the mean-field corollary. There are no fitted free parameters: L and the rate C = 2 max(1,L) are defined from W, not fit to data.

axioms (7)
  • domain assumption AssW: W : R^d -> R is even, C^{1,1}, with globally Lipschitz gradient of constant L
    Assumption 1; the whole development is parameterized by this regularity. Without it the Newton-to-Vlasov passage is not classical (singular forces are open).
  • domain assumption AssW2: grad W in C^1 (W in C^2), one field beyond AssW
    Assumption 2; the superposition principle (Theorem 1.7) needs C^1 dependence of the flow on initial point. The paper explicitly says only this bridge pays for AssW2.
  • domain assumption Short-window condition L*T^2 < 1 (LocalSmallness_PL_buffer L T)
    Theorem 1.7 hypothesis; the weak-to-Lagrangian bridge is proved only on short windows; chaining to arbitrary T is declared future work.
  • domain assumption Force-field continuity hypotheses and uniform moment bound M_rho in Theorem 1.7
    hf_cont and hf_cont_deriv reproduced in full in Appendix A; these are properties of the solution f itself, not generic.
  • domain assumption DobrushinStabilityEstimate for the empirical curve vs Vlasov solution is assumed in meanFieldLimit, not derived in Lean
    Appendix A: meanFieldLimit has hDobrushin as an explicit hypothesis; Section 3.3 says Theorem 1.5 supplies it, but no reported Lean theorem discharges it for the Newtonian empirical curve.
  • standard math Mathlib v4.29.1 background facts: Farkas/conic separation, Gronwall's inequality, measure/ENNReal infrastructure
    Farkas cited to [21]; gronwall_mild_le named in Section 3.3; these are library facts assumed as ambient, not proved in the paper.
  • standard math Deferred external fact: Polish-space completeness of the Wasserstein metric
    Section 4.4; deferred as a cited placeholder off every certified path, so the target theorems do not depend on it.

pith-pipeline@v1.3.0-alltime-deepseek · 20974 in / 21552 out tokens · 220940 ms · 2026-08-02T07:43:14.632783+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.08986 by Joseph K. Miller.

Figure 1
Figure 1. Figure 1: A roadmap of the development: the project blueprint’s dependency graph, auto-extracted from the elaborated Lean proof terms — boxes are definitions, ellipses theorems, green fully formalized. The interactive version, with statements and proof sketches on every node, is at hydrodynamical.github.io/Vlasov_Meanfield_Formalization. its tools: the rules name no particular system and no division of labor, so wha… view at source ↗
Figure 2
Figure 2. Figure 2: From the case study of Section 3 (362 commits): live sorry count per production file, stacked so the leaves sum to the total (black line). The open-goal front is concentrated in one active leaf at a time and migrates across the development; the total peaks at 24 and returns to 0. The two humps are two games — the well-posedness/stability marquee and the superposition-principle follow-on — separated by the … view at source ↗
Figure 3
Figure 3. Figure 3: From the case study of Section 3: named strategies present in the standing instruction file G across its 36 revisions, by series (L/P/M/B). The staircase shape — flats punctuated by jumps at specific failures — is the signature of strategies earned rather than designed. The total grows 4 → 34; the four-series taxonomy crystallizes in one revision, and the process (P) series jumps by four in the aftermath o… view at source ↗
Figure 4
Figure 4. Figure 4: From the case study of Section 3: all 362 commits classified by primary intent. Roughly one in seven is pure meta-knowledge capture (discipline / lessons) — a direct, if heuristic, measure of the meta-learning loop, distinct from the proof work itself. 4.2 Timeframe and the division of labor The well-posedness and stability marquee — from the first translated theorem to the certified stability estimate — r… view at source ↗

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory

    cs.LO 2026-07 conditional novelty 5.0

    An ongoing Lean formalization of Shum's probability textbook, using AI-assisted translation and bridge lemmas, has uncovered a textbook error.

Reference graph

Works this paper leans on

36 extracted references · 15 linked inside Pith · cited by 1 Pith paper

  1. [1]

    Commelin, A

    J. Commelin, A. Topaz, et al., The Liquid Tensor Experiment , Lean 3 formalization, https: //github.com/leanprover-community/lean-liquid (completed 2022); see also J. Commelin 24 and A. Topaz, Abstraction boundaries and spec driven development in pure mathematics , arXiv:2309.14870

    Pith/arXiv arXiv 2022

  2. [2]

    T. Tao, Y. Dillies, B. Mehta, et al., Formalizing the proof of the polynomial Freiman–Ruzsa conjecture in Lean 4 , https://github.com/teorth/pfr (2023)

    2023

  3. [3]

    Becker, M

    L. Becker, M. I. de Frutos-Fernández, L. Diedering, et al., A blueprint for the formalization of Carleson ’s theorem on convergence of Fourier series , arXiv:2405.06423 (2025)

    Pith/arXiv arXiv 2025

  4. [4]

    van Doorn, P

    F. van Doorn, P. Massot, O. Nash, Formalising the h-principle and sphere eversion , in Proc. 12th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs (CPP 2023) , 121–134; arXiv:2210.07746

    Pith/arXiv arXiv 2023

  5. [5]

    Massot, Leanblueprint, software, https://github.com/PatrickMassot/leanblueprint

    P. Massot, Leanblueprint, software, https://github.com/PatrickMassot/leanblueprint

  6. [6]

    Hubert, R

    T. Hubert, R. Mehta, L. Sartran, et al. (Google DeepMind), Olympiad-level formal mathemat- ical reasoning with reinforcement learning , Nature 651 (2026), 607–613, https://doi.org/10 .1038/s41586-025-09833-y

    2026

  7. [7]

    Tsoukalas, A

    G. Tsoukalas, A. Kovsharov, S. Shirobokov, et al. (Google DeepMind), Advancing mathematics research with AI-driven formal proof search , arXiv:2605.22763 (2026)

    Pith/arXiv arXiv 2026

  8. [8]

    Harmonic, Aristotle: IMO-level automated theorem proving , arXiv:2510.01346 (2025)

    Pith/arXiv arXiv 2025

  9. [9]

    Sothanaphan, Resolution of Erdős Problem #728: a writeup of Aristotle’s Lean proof , arXiv:2601.07421 (2026)

    N. Sothanaphan, Resolution of Erdős Problem #728: a writeup of Aristotle’s Lean proof , arXiv:2601.07421 (2026)

    arXiv 2026

  10. [10]

    Zhang, Y

    Y. Zhang, Y. Sun, T. Suzuki, J. D. Lee, F. Liu, LeanMarathon: toward reliable AI co- mathematicians through long-horizon Lean autoformalization , arXiv:2606.05400 (2026)

    Pith/arXiv arXiv 2026

  11. [11]

    Alexeev, K

    B. Alexeev, K. Barreto, Y. Li, J. D. Lichtman, L. Price, J. I. Shah, Q. Tang, T. Tao, Primitive sets and von Mangoldt chains: Erdős problem #1196 and beyond , arXiv:2605.00301 (2026)

    Pith/arXiv arXiv 2026

  12. [12]

    Ilin, Semi-autonomous formalization of the Vlasov–Maxwell–Landau equilibrium , arXiv:2603.15929 (2026)

    V. Ilin, Semi-autonomous formalization of the Vlasov–Maxwell–Landau equilibrium , arXiv:2603.15929 (2026)

    arXiv 2026

  13. [13]

    M. R. Douglas, S. Hoback, A. Mei, R. Nissim, Formalization of QFT, arXiv:2603.15770 (2026)

    arXiv 2026

  14. [14]

    Armstrong, J

    S. Armstrong, J. Kempe, Formalization of De Giorgi–Nash–Moser theory in Lean , arXiv:2604.05984 (2026)

    Pith/arXiv arXiv 2026

  15. [15]

    Bertolini, J

    S. Bertolini, J. de Dios Pont, B. Pineau, J. P. G. Ramos, M. A. Taylor, L2-stability for STFT phase retrieval , arXiv:2605.20527 (2026)

    Pith/arXiv arXiv 2026

  16. [16]

    Abdalla, J

    P. Abdalla, J. de Dios Pont, J. P. G. Ramos, M. A. Taylor, Stable phase retrieval for spans of independent random variables , arXiv:2607.06693 (2026)

    Pith/arXiv arXiv 2026

  17. [17]

    de Dios Pont, L

    J. de Dios Pont, L. Liehr, M. A. Taylor, On the existence problem of regular Gabor frames , arXiv:2606.26052 (2026)

    Pith/arXiv arXiv 2026

  18. [18]

    de Dios Pont, L

    J. de Dios Pont, L. Liehr, M. A. Taylor, Cantor measures with odd base do not admit Fourier frames, arXiv:2607.08656 (2026)

    Pith/arXiv arXiv 2026

  19. [19]

    Zimmer, N

    M. Zimmer, N. Pelleriti, C. Roux, S. Pokutta, The Agentic Researcher: a practical guide to AI-assisted research in mathematics and machine learning , arXiv:2603.15914 (2026). 25

    arXiv 2026

  20. [20]

    A vigad, Mathematicians in the age of AI , arXiv:2603.03684 (2026)

    J. A vigad, Mathematicians in the age of AI , arXiv:2603.03684 (2026)

    Pith/arXiv arXiv 2026

  21. [21]

    9th ACM SIGPLAN Int

    The mathlib Community, The Lean mathematical library , in Proc. 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs (CPP 2020) , 367–381

    2020

  22. [22]

    R. L. Dobrushin, Vlasov equations , Funct. Anal. Appl. 13 (1979), 115–123

    1979

  23. [23]

    Braun, K

    W. Braun, K. Hepp, The Vlasov dynamics and its fluctuations in the 1/N limit of interacting classical particles, Comm. Math. Phys. 56 (1977), 101–113

    1977

  24. [24]

    Villani, Optimal Transport: Old and New , Grundlehren der mathematischen Wissenschaften 338, Springer, 2009

    C. Villani, Optimal Transport: Old and New , Grundlehren der mathematischen Wissenschaften 338, Springer, 2009

    2009

  25. [25]

    Ambrosio, N

    L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Prob- ability Measures, 2nd ed., Birkhäuser, 2008

    2008

  26. [26]

    Spohn, Large Scale Dynamics of Interacting Particles , Springer, 1991

    H. Spohn, Large Scale Dynamics of Interacting Particles , Springer, 1991

    1991

  27. [27]

    Golse, On the dynamics of large particle systems in the mean field limit , in Macroscopic and Large Scale Phenomena , Lect

    F. Golse, On the dynamics of large particle systems in the mean field limit , in Macroscopic and Large Scale Phenomena , Lect. Notes Appl. Math. Mech. 3, Springer, 2016, 1–144

    2016

  28. [28]

    Neunzert, An introduction to the nonlinear Boltzmann–Vlasov equation , in Kinetic Theories and the Boltzmann Equation , Lecture Notes in Math

    H. Neunzert, An introduction to the nonlinear Boltzmann–Vlasov equation , in Kinetic Theories and the Boltzmann Equation , Lecture Notes in Math. 1048, Springer, 1984

    1984

  29. [29]

    Hauray, P.-E

    M. Hauray, P.-E. Jabin, Particle approximation of Vlasov equations with singular forces: propa- gation of chaos , Annales scientifiques de l’École normale supérieure 48 (2015), fasc. 4, 891–940

    2015

  30. [30]

    Lazarovici, P

    D. Lazarovici, P. Pickl, A mean field limit for the Vlasov–Poisson system , Arch. Ration. Mech. Anal. 225 (2017), 1201–1231

    2017

  31. [31]

    Feistl-Held, P

    M. Feistl-Held, P. Pickl, On the mean-field limit for the Vlasov–Poisson system , arXiv:2504.01471 (2025)

    Pith/arXiv arXiv 2025

  32. [32]

    Feistl-Held, P

    M. Feistl-Held, P. Pickl, On the mean-field limit for the Vlasov–Poisson system in two dimen- sions, arXiv:2509.17821 (2025)

    arXiv 2025

  33. [33]

    Serfaty, Mean field limit for Coulomb-type flows , Duke Math

    S. Serfaty, Mean field limit for Coulomb-type flows , Duke Math. J. 169 (2020), no. 15, 2887– 2935

    2020

  34. [34]

    Nguyen, M

    Q.-H. Nguyen, M. Rosenzweig, S. Serfaty, Mean-field limits of Riesz-type singular flows , Ars Inven. Anal. (2022), Paper No. 4, 45 pp

    2022

  35. [35]

    Nguyen, S

    Q.-H. Nguyen, S. Serfaty, Singular mean-field limits via a multiscale mollification metric , arXiv:2607.10686 (2026)

    Pith/arXiv arXiv 2026

  36. [36]

    J. K. Miller, A. R. Nahmod, N. Pavlović, M. Rosenzweig, G. Staffilani, A rigorous derivation of the Hamiltonian structure for the Vlasov equation , Forum Math. Sigma 11 (2023), e77. 26

    2023