Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean
A Lean proof, registered on Palomar, that some countable group has measurably isomorphic Bernoulli shifts over alphabets of different sizes, so that base entropy is not an isomorphism invariant for that group; the group comes from OpenAI's claimed counterexample to Kaplansky's direct-finiteness conjecture, and the dynamical construction was written with GPT-6 Astra and GPT-6 Sol under Peter Burton's direction.
- Lab
- Independent
- Model
- GPT-6 Astra and GPT-6 Sol via Codex, building on an OpenAI construction
- Field
- Mathematics
- Date
- 2026-10-27
- Human collaborators
- Peter Burton
What was found
For a countable group and a finite alphabet , the Bernoulli shift is acting by translation on with the uniform product measure. Ornstein showed in 1970 that base entropy is a complete invariant of these shifts over the integers, and Bowen showed in 2010 that it is an isomorphism invariant over every sofic group, so shifts with different base entropies can be isomorphic only over a group outside that class. The registered theorem gives a countable group and a nontrivial finite alphabet for which the shifts on and on are equivariantly isomorphic on invariant conull sets, with a measurable inverse. The group and the algebraic input come from OpenAI's manuscript A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two, whose abstract says the group is non-sofic; its Lean development is imported at a pinned commit, and this project builds the dynamical conjugacy on top of it.
Novelty check
arXiv, 2026-10-29: abs:"Bernoulli shifts" AND abs:"entropy" AND abs:"sofic" returned 11 records, on sofic entropy and its refinements; none constructs isomorphic shifts with different base entropies. Such an example needs a non-sofic group, and whether any group is non-sofic was itself open until OpenAI's Kaplansky manuscript claimed one. Within this registry that manuscript is part of 2026-10-06-openai-math-collection with no entry of its own, and nothing covers this result. The 2026-10-29 watch run surfaced it through its Palomar registration.
Caveats and known objections
Graded formal on the Palomar registration: the repository reports that Palomar's mechanical verification passed at the registered commit, including Lean kernel checking and an independent NanoDa replay, and its comparator configuration enables NanoDa. A scan of all 59 Lean files at that commit found no axiom declarations, no native_decide, and sorry only in the Challenge.lean statement file. The grade covers less than the expository note: the metadata says the certificate concerns finite-uniform measurable conjugacy only, does not certify the all-base collapse, finitary continuity, the integer coding inputs or the note's later corollaries, and claims no formal entropy classification theorem. The formalization.yaml at the registered commit still says the revision had not completed Palomar's hosted preflight and claims no registration; the README, updated afterwards, explains that those notes predate the hosted checks. Because OpenAI's Lean proof of the algebraic input builds inside this development, the formal grade covers it too, but the mathematics it encodes is an unrefereed manuscript from an unreleased model, and no mathematician is on record as having read either argument. Review is recorded as agent-reviewed with no human peer review, and the expository note comes from a draft GPT-6 wrote. Autonomy is collaborative: the metadata credits GPT-6 Astra and GPT-6 Sol with mathematical writing, Lean implementation, integration and source review under human direction, and the decisive algebraic input is another lab's model's work.
Machine-checked elsewhere
PalomarFinite uniform Bernoulli shifts with unequal base entropy
PALOMAR-2026-10-27-000030 · peterburton1728/bernoulli-iso-1 at 80241ef9354d · checked 2026-10-27
ProvedBernoulliCertificate.unequal_finite_bernoulli_shifts
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Permitted axioms are exactly propext, Classical.choice and Quot.sound, with NanoDa enabled. The certificate is narrower than the expository note.
No independent check is recorded on this entry yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-27-bernoulli-shifts-unequal-entropyBibTeX
@misc{whataifound-independent-2026-entropy,
title = {Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-10-27-bernoulli-shifts-unequal-entropy}
}