The unit group of the binary Leavitt algebra L_F₂(1,2) is not sofic
Queued record · four gates mapped · no examination route has run
Current record status
What this docket currently establishes
Queued record · four gates mapped · no examination route has run. This docket identifies what has been checked and what remains open. It does not validate or reject the manuscript's headline claim beyond the explicitly stated scope.
- Claim
- The unit group of the binary Leavitt algebra L_F₂(1,2) is not sofic
- Source version
- Updated Ten Advances manuscript · updated 2026-08-06
- Source SHA-256
ebc561ab5c53dbd240e17a8fdb6fffeb648591eca85dbfc7466f563638f8c566- Source locked
- Last material update
- Next open step
- Reconcile the substantively revised August 6 prose with the August 2 Lean commit before any formal replay is treated as relevant
- Machine-readable record
- JSON record · Atom change feed
One-minute summary
Chapter 3 of OpenAI's updated Ten Advances manuscript claims that the binary Leavitt algebra's unit group is not sofic. The pinned Lean commit predates a substantive prose revision by four days. Paper-to-Lean and version correspondence is therefore the first gate; no build or mathematical examination has run.
For non-specialists
Why this matters
A nontechnical reading of the claim and its possible consequences. These are implications to consider, not findings of this docket.
In plain English
The manuscript claims that the group of invertible elements of a particular algebra cannot be approximated by finite models in the sense captured by soficity. The prose was revised after the linked Lean artifact was created, and no formal or mathematical examination has yet run here.
If the claim holds
If the claim holds, it would provide a group that does not have the stated finite-approximation property. That is a mathematical consequence about the defined group, not a conclusion about downstream uses of the algebra.
Potential concerns
The first issue is whether the earlier Lean artifact actually matches the revised manuscript's definitions and endpoint. The proof also depends on specialized claims about expanders, group approximations, and the algebra's unit group.
If it does not hold up
If the revised argument does not hold, the earlier formal artifact may still be relevant to a different statement, but it would not establish the revised public claim without a demonstrated correspondence.
Scope of this docket
The planned examination covers original-to-revised source lineage, paper-to-Lean correspondence, a fresh pinned formal replay, the exact hypotheses of cited theorems, and an independent specialist reconstruction of the revised proof.
Claim and dependency map
Paper-to-Lean and August 2/August 6 version correspondence
Depends on: original PDF · revised PDF · pinned commit
Fresh pinned formal replay and axiom closure
Depends on: G1
Cited-theorem hypothesis table
Depends on: primary literature
Independent examination of the revised expander and Leavitt-algebra route
Depends on: G1 · G3
Examination routes
- formal
- Queued · updated 2026-08-26
Planned: build and kernel-check the pinned Lean target, then keep its result separate from prose correspondence. - literature
- Queued · updated 2026-08-26
Planned: exact-hypothesis table for every load-bearing cited theorem. - expert
- Queued · updated 2026-08-26
Planned: independent group-theory reconstruction of the August 6 proof route.
Findings and scope limits
No Lean build, replay, or mathematical examination route has run in this lab.
The August 2 Lean commit predates the substantive August 6 manuscript revision, so repository proximity cannot establish correspondence.
Open Steps—where expert eyes are needed
Which exact Lean endpoints, witnesses, and definitions correspond to the revised paper's unit-group claim?
The formal artifact predates the revised proof and may encode a materially different route or endpoint.
Source record and provenance
The updated Chapter 3 is the examination target. The original PDF is preserved separately. No journal or referee disposition is asserted in the locked sources.
Selected and maintained by Material Shift as protocol research. No external sponsor or author involvement is recorded for this case.
Retrieved .
- Preservation
- The manuscript and commit-pinned Lean artifact are separately identified. A dated Wayback reference was found, but availability is intermittent and its bytes have not been hash-compared with the locked docket file.
- Record provenance
- Claim map and route plan prepared by Material Shift from the recorded public sources; no mathematical finding or external review is recorded.
- Author contact
- No author outreach, correspondence, response, or author approval is recorded for this docket. Contact the record steward.
Version and record history
-
record provenance
2026-08-01-openai-nonsofic-group
Record classified as queued; source preservation, route provenance, and author-contact state published
-
new docket
2026-08-01-openai-nonsofic-group
Updated and original manuscripts plus Lean commit locked; four gates mapped; no gate run
-
source updated
2026-08-01-openai-nonsofic-group
OpenAI published a substantive Chapter 3 revision; the August 2 Lean commit predates it
Statuses describe evidence collected for a defined scope. They are not peer-review decisions, publication recommendations, or certificates of mathematical truth.