# Isomorphism of the free group factors

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [An isomorphism of the free group factors](../../preprints/An-isomorphism-of-the-free-group-factors-September-23-2026/An-isomorphism-of-the-free-group-factors-September-23-2026.pdf)

## Scope

The free group factor problem asks whether the von Neumann algebras of free groups of different ranks are isomorphic. The formalization proves that interpolated free group factors with any parameters $r,s>1$, including the infinite parameter, are normally trace-preservingly isomorphic. The paper's fundamental-group conclusion is a further consequence rather than a separate selected statement here.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Isomorphism of all interpolated free group factors | [InterpolatedFactors.lean](../ComparatorChallenges/InterpolatedFactors.lean) |