Two notions of free entropy differ even when both are finite

Proves two standard notions of free entropy can differ by at least 1/2 even when both are finite.

1 paper September 25, 2026 Explained by AI

Free entropy measures how much room a family of noncommuting variables has, much as ordinary entropy does for random numbers. Voiculescu gave two definitions: one counts nearby matrix models, the other tracks added noise. They agree for one variable, and a known question asked if they agree whenever the first is finite. This paper builds a family where both are finite but differ by at least one half, and Lean checks it. The family uses a large number of variables.

First step

1994

Voiculescu, who defined microstates free entropy (1994) and later nonmicrostates free entropy (1998)

Significance

Major

It answers negatively the finite-entropy form of a question in Voiculescu's free-entropy unification problem, with a Lean check.

Trust

Formal proof listed

Field

Operator algebras

1 paper

The explanation

Start with random matrices. Fill a large d-by-d Hermitian matrix with Gaussian entries of variance 1, the GUE ensemble. In the paper's normalization, its entropy per entry is ½·log(2πe), about 1.419. Take a second, independent GUE coordinate of variance 4. Its value is ½·log(8πe), about 2.112. Independent coordinates add, so the pair has entropy about 3.531Source 1. Entropy here measures spread: more variance, more room.

Free probability studies variables that do not commute, like large matrices. Free entropy measures their room. Voiculescu gave two definitions. The microstates entropy χ counts the volume of matrix tuples whose trace moments match the variables. The nonmicrostates entropy χ* instead adds free semicircular noise, the noncommutative bell curve, and integrates an information measure along the waySource 2. The two agree for a single variable. Whether they agree in general was part of Voiculescu's unification problemSource 3. Biane, Capitaine and Guionnet proved χ ≤ χ* in generalSource 4. Equality was known in regular convex settings. The finite-entropy question asked: if χ is finite, must χ equal χ*?

The paper answers noSource 5. It builds a bounded tuple X with χ finite and χ at most χ* − ½Source 6. The gap of ½ is about a third of the one-variable value 1.419 above. The construction mixes free semicircular variables with one coordinate Y that is spread evenly over p points in [−1, 1]. With p = 3, those points are −1, 0 and 1. Y commutes with the others and splits their energy into blocks. A small dose of free noise makes χ finite while keeping that block structureSource 7.

The obstacle is to show the two entropies see the block structure differently. After more noise, χ* becomes close to that of plain semicircular variables. Matrix models keep detectable blocks, which costs them volume. The noise time t = p^(3/4) balances the two estimates as p growsSource 8. For p = 16, that gives t = 8. The example needs a large but fixed number of variables. It says nothing about smaller numbersSource 9.

How sure is this? Lean, a computer proof checker, has a formal statement of the main theorem: a bounded tuple with χ finite and χ ≤ χ* − ½. So the paper proves this, as far as the Lean statement matches the paper. No specialist review is published.

What it doesn't show. This does not settle the question for small numbers of variables, and it does not address cases where the microstates entropy is minus infinity.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

A clean negative answer to a named question, with a Lean check. It needs many variables and leaves small numbers of variables open. No specialist review is published.

Words used

Free probability: A theory of noncommuting random variables, such as large random matrices, with freeness in place of independence.
Self-adjoint tuple: A list of operators each equal to its own adjoint, the analogue of real random variables.
Microstates free entropy χ: A measure of the volume of matrix tuples whose trace moments approximate those of the variables.
Nonmicrostates free entropy χ*: A free entropy defined by adding free semicircular noise and integrating free Fisher information.
Semicircular variable: The free-probability analogue of a Gaussian; its eigenvalue density is a semicircle.
GUE: Random Hermitian matrices with independent Gaussian entries, whose eigenvalues follow the semicircle law.
Tracial state: A positive normalized linear functional τ with τ(xy) = τ(yx), playing the role of an expectation.

The original paper

A finite-entropy separation of microstates and nonmicrostates free entropy (PDF, opens in a new tab)
September 25, 2026

Lean notes

All quoted lines (9)

Thus independent GUE coordinates of variances $w_i>0$ have normalized entropy $\frac12\sum_i\log(2\pi e w_i)$ .
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
His nonmicrostates free entropy $\chi^*(X)$ instead uses conjugate variables, the free analogues of classical scores, and integrates free Fisher information along addition of freely independent semicircular noise.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
The two quantities agree for a single self-adjoint variable, and their agreement for general tuples was one of the questions in Voiculescu's unification problem.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
Biane, Capitaine, and Guionnet proved the general comparison $\chi\leq\chi^*$ through large-deviation bounds for matrix Brownian motion.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
We answer the finite-entropy equality question for microstates and nonmicrostates free entropy negatively.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
We construct a bounded self-adjoint tuple $X$ in a von Neumann algebra with faithful normal tracial state such that $-\infty<\chi(X)\leq\chi^*(X)-\tfrac12<\infty$ .
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
A small perturbation $X=C+\sqrt h S$ has finite microstates entropy, while its last coordinate still determines spectral blocks containing much of the energy of the first $p$ coordinates.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
The choice $t=p^{3/4}$ satisfies both conditions as $p\to\infty$ .
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text
It does not address equality for every smaller prescribed number of variables.
A finite-entropy separation of microstates and nonmicrostates free entropy Back to text

Other sources

openai/math, Lean scope note for family 298 The formalization disproves equality of microstates and nonmicrostates free entropy even when both quantities are finite.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

291Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stabilityOperator algebras
297A ZFC counterexample to Naimark's problemOperator algebras
299The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stabilityOperator algebras
296The generator problem for finite factorsOperator algebras
300Approximation and quadratic strong-operator pavingOperator algebras

Browse Operator algebras Open since the 1990s Lean-checked results