What was already known
Prior transformer-expressivity work gives lower bounds and studies related architectures. Hsu and Xu obtain a concurrent symmetric-function characterization without positional embeddings; Rajaraman and collaborators also study head complexity. This record covers the stated additive token/position model and its autonomous core, without claiming exclusive priority.
AI involvement
Karthik Viswanathan and colleagues report that GPT-5.6 Sol derived the normal form, threshold-degree bound and exact symmetric characterization in about 9.5 hours after a problem-setting prompt, with no subsequent human mathematical lemmas or corrections. Humans specified the model and acceptance criteria, then selected and checked the formal statements and reorganized the code.
Importance
Provides exact architectural-resource bounds in a well-defined Boolean attention model, including a normal-form characterization and matching symmetric-function bounds.
Limitations
The model has one attention layer, unrestricted model/head dimensions, a fixed query token and linear readout. It excludes feed-forward layers, layer normalization and claims about training or full language-model capability. The later ten-bit separation involved an additional human-directed search and is outside this autonomous-core record.
Technical verification
The paper reports complete Lean checking of the core results and expert review of statement fidelity. The pinned formalization maps the normal-form and symmetric-head theorems to exact Lean declarations; the checking execution date is undocumented.
Formal checking
The paper reports complete Lean checking of the core results and expert review of statement fidelity. The pinned formalization maps the normal-form and symmetric-head theorems to exact Lean declarations; the checking execution date is undocumented.
- Checker
- Project authors: Lean 4 kernel checks and expert statement review
- Scope
- The general-n core theorems, including HStar_eq_Lfrac and HStar_symmetricFn_eq_signChanges, under the formalized head model. The project reports only standard Lean axioms; the paper describes human expert statement-fidelity review.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
No named human account explaining the scoped central reasoning was established. Few is the documentation default, not a finding that people cannot understand it.
Correction and publication history
Added the sourced result with its exact hypotheses, prior work, AI contribution and checking scope.
Read this published revision