The unit group of the binary Leavitt algebra L_F₂(1,2) is not sofic
Intake record · four gates mapped · no audit gate has run
Current record status
What this docket currently establishes
Intake record · four gates mapped · no audit gate 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
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 audit has run.
Scope of this docket
The planned audit 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 audit of the revised expander and Leavitt-algebra route
Depends on: G1 · G3
Evidence routes
- formal
- Planned: build and kernel-check the pinned Lean target, then keep its result separate from prose correspondence.
- literature
- Planned: exact-hypothesis table for every load-bearing cited theorem.
- expert
- Planned: independent group-theory reconstruction of the August 6 proof route.
Findings and scope limits
No Lean build, replay, or mathematical audit gate 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 audit 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 .
Version and record history
-
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.