Equality of microstates and nonmicrostates free entropy
From OpenAI Aftermath
Voiculescu defined two free entropies for a tuple of self-adjoint operators in a tracial von Neumann algebra: the microstates entropy χ, from the volumes of matrix tuples approximating the joint moments, and the nonmicrostates entropy χ*, from free Fisher information along the addition of free semicircular noise. Whether χ = χ* whenever χ is finite was part of his unification problem. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a tuple for which both are finite and differ, with a Lean formalization of the main theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The two entropies agree for a single variable, and their agreement for general tuples was one of the questions in Voiculescu's unification problem. Guionnet stated the finite-entropy formulation as a conjecture; Jekel and Pi discussed nonapproximable laws with χ = −∞ < χ*.
- Biane, Capitaine and Guionnet proved χ ≤ χ* in general, and Jekel and Pi gave an elementary proof through classical entropy and Fisher information. Equality is known in regular convex settings, by Dabrowski for a class of strictly convex potentials and by Jekel for convex matrix potentials with suitable regularity.
The original result
- Claim. Theorem 1.1 of A finite-entropy separation of microstates and nonmicrostates free entropy states that there are an integer n ≥ 2 and a bounded self-adjoint tuple X in a von Neumann algebra with faithful normal tracial state such that −∞ < χ(X) ≤ χ*(X) − 1/2 < ∞, where χ uses an operator-norm cutoff and a limsup over matrix sizes. The number of variables is large but fixed; the manuscript does not address smaller prescribed numbers of variables.
- Method, as described: the tuple is a small free semicircular perturbation of free semicircular variables together with a commuting variable uniformly distributed on equally spaced points. After further noise, a cumulant estimate brings χ* close to that of a semicircular family, while matrix microstates keep a detectable block structure that independent GUE matrices lack; the classical-to-free Fisher comparison of Jekel and Pi transfers the resulting deficit between the scales.
- Sources. The manuscript A finite-entropy separation of microstates and nonmicrostates free entropy at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization disproves equality of the two entropies even when both are finite, constructing a bounded self-adjoint tuple with −∞ < χ(X) ≤ χ*(X) − 1/2 < ∞ for a fixed finite number of variables. The Comparator statement is
FiniteEntropySeparation.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statement) | Rates the family "full"; lists the hand-written definitions of the microstates entropy with cutoff, free Fisher information and the nonmicrostates entropy among the definitions to check, and records a sandboxed Comparator pass for FiniteEntropySeparation. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the FiniteEntropySeparation solution, in 997 s. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list FiniteEntropySeparation, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_519 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer read all six sections and checked the normalizations of both entropies, the free-flow identity, the Wick-testing lemma, the cumulant and sparsity bounds, the explicit parameters, the finite-time flow lemma and the matrix block estimate. | Part of an audit that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-21 (listed) | D. Jekel, On counterexamples to the unification of free entropy (arXiv:2610.27243) | Extension (exposition; Fisher information) | Describes OpenAI's manuscript as the first example with −∞ < χ < χ*, gives a detailed presentation of a similar example, and shows explicitly the separation between free Fisher information and the large-n limit of classical Fisher information through the relationship with Wasserstein distance. | arXiv preprint. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
