Archive DOI: 10.5281/zenodo.22770864. This identifier is assigned to this edition; Zenodo publication was pending when these files were prepared. The PDF and matching source archive are available above.
An affirmative answer
There is a nontrivial finite group of odd prime-power order whose full automorphism group has the same order.
Theorem. The explicit construction in the paper gives a finite group \(G\) with
This answers D. MacHale’s existence question in Kourovka Notebook 16.63.
The group is specified by 31 coordinates modulo \(1009^{1689}\), an explicit integer Lie bracket, and the finite Baker–Campbell–Hausdorff multiplication rule. Its nilpotency class is at most 846, below the prime 1009. No minimality claim is made for its prime or order.
Why the count includes every automorphism
The construction starts with a 31-dimensional Lie algebra based on an Omirov–Ruan template. A choice of lattice forces every automorphism of the finite Lie ring to preserve a rigid flag after reduction modulo 1009. Integral logarithms then turn the full automorphism condition into an exact linear equation.
The resulting integer matrix has 14,415 rows, 961 columns, rank 931, and nullity 30. Its nonzero Smith invariants have the following valuations at 1009:
| Valuation | 0 | 1 | 2 | 3 | 4 |
|---|---|---|---|---|---|
| Multiplicity | 87 | 55 | 758 | 6 | 25 |
The valuation sum is 1689. At depth \(i\geq7\), the full Lie-ring automorphism count is \(1009^{30i+1689}\). Choosing \(i=1689\) makes this equal to the number of elements, \(1009^{31i}\). The Lazard correspondence preserves the full automorphism group because the class is strictly less than the prime.
Reproduce the checks
Download and extract the source package, then run this command from its folder:
python3 scripts/resume.pyThis needs Python 3 and a C++17 compiler supporting 128-bit integers. The verifier reconstructs the brackets and matrix from formulas, replays the exact certificate, checks small-group controls, and confirms that a corrupted certificate is rejected. For full Python regeneration with NumPy and SymPy installed, use python3 scripts/resume.py --full.
Separate AI audit agents independently reviewed the finite-field automorphisms, the congruence and logarithm arguments, and the computation. The package contains their reports and fresh reproduction records. The mathematical argument also uses proofs that are outside the scope of the executable checks.
Paper review status: the computational checks and AI reviews described above were completed, with no unresolved error identified within their stated scope. The full theorem has not undergone external human peer review or complete proof-assistant verification.
Lean companion: partial formalization
The accompanying Lean development supplies formal definitions and proofs for ingredients of the construction. The full finite-group theorem remains unformalized. The source was audited locally after its original delivery, with compiler repairs and reproducible build evidence included in the download.
The 18 September 2026 audit compiled all 142 current modules and inspected the actual types and transitive axiom dependencies of 1,262 named declarations. The only reported axioms are Lean’s standard foundational axioms. The report records the checked scope, source comparison, and trust limits.
The remaining developments include the general finite-quotient lifting argument, the complete exponential/logarithm bijection, acceptance of the actual Smith certificate, and the BCH group construction with its full group/Lie automorphism correspondence. The challenge propositions in the source state the intended final result but do not prove it.
Download the partial Lean source and audit · Read the Lean verification report. See the companion README for the exact checked scope, remaining obligations, and pinned build instructions. This supplement does not change the version 1.1.0 paper or its archived certificates.
Attribution and scope
Author: Alec Kriebel. AI disclosure: The construction, proof development, and initial verification software were generated using ChatGPT-6 Astra Pro. Separate Codex sessions performed additional AI-assisted reviews and exact computational checks. These checks do not constitute external human peer review or a complete proof-assistant formalization.
The underlying Lie-algebra template is credited to Omirov and Ruan, Theorem 4.8. The paper supplies its integer normalization, the required finite-characteristic arguments, the asymmetric lattice, and the exact full finite-automorphism count. The literature audit distinguishes this equality problem from the earlier divisibility conjecture in Archive 12.77.
A focused literature search found no earlier resolution of the exact question. This is a bounded search finding, not a guarantee of bibliographic priority. Full references and the audit trail accompany the paper.