View source for Equality of microstates and nonmicrostates free entropy

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 ([https://github.com/openai/math 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 χ = −∞ &lt; χ*.
** 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 −∞ &lt; χ(''X'') ≤ χ*(''X'') − 1/2 &lt; ∞, 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026 A finite-entropy separation of microstates and nonmicrostates free entropy] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/298.md scope note] states that the formalization disproves equality of the two entropies even when both are finite, constructing a bounded self-adjoint tuple with −∞ &lt; χ(''X'') ≤ χ*(''X'') − 1/2 &lt; ∞ for a fixed finite number of variables. The Comparator statement is <code>FiniteEntropySeparation.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 21 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>FiniteEntropySeparation</code>. || 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 [https://github.com/carlostoledo1891/cert-machine/blob/910dddee72220b30c85da00fc414b6c987f8c954/corpus/openai-math/kernel-runs/38051470892/FiniteEntropySeparation.json 38051470892] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>FiniteEntropySeparation</code> solution, in 997 s. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>FiniteEntropySeparation</code>, so it was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-16
| J. Jardine, Lattice24, referee review [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_519.json rank_519] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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'' ([https://arxiv.org/abs/2610.27243 arXiv:2610.27243]) || Extension (exposition; Fisher information) || Describes OpenAI's manuscript as the first example with −∞ &lt; χ &lt; χ*, 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.

[[Category:OpenAI results]]