Nilradical
A mathematical research agent with answers to eight Kourovka Notebook problems in group theory. Each has a complete Lean 4 proof replayed by an independent checker, and a statement accepted by a human reviewer.
Results
Affirmative and negative answer the question as posed. Records give precise statements, Lean sources and verification.
-
16.68
Word maps over the real and complex numbers
Every nontrivial two-variable word map on PSL₂(ℂ) is surjective; an explicit word map on PSL₂(ℝ) omits every nonidentity involution.
-
21.3
Separating soluble subgroups
For symmetric and alternating groups in every sufficiently large degree, any two soluble subgroups have a conjugate with trivial intersection.
-
21.35
An order criterion for multilinear verbal subgroups
For every multilinear commutator word in a finite group, an order condition on individual word values characterizes when the verbal subgroup has a normal p-complement.
-
21.38
An infinite group of spread one
An explicit subgroup of Thompson’s group F is infinite and has ordinary spread exactly one.
-
21.44
Dense generators with slow growth
A fixed pair generates a dense subgroup of subexponential growth in the infinite iterated natural degree-five alternating wreath product.
-
21.53
Two colours do not determine the rest
In a finite simple matrix group over GF(8), a swap on an entire involution class preserves product orders 2 and 3 but changes an edge from order 5 to order 7.
-
21.68
A semiabelian group that is not monomial
A semiabelian group of order 2,592 has an irreducible nonmonomial complex representation of degree eight.
-
21.106
Two formula values, an infinite subgroup
A parameter-free first-order formula has exactly two values generating an infinite subgroup in the residually finite integral Heisenberg group.
How a result is produced and checked
- Novelty. A dated literature search confirms the question is open; it is refreshed before release.
- Exploration and falsification. Candidate ideas are developed, then attacked with exact computation in search of counterexamples.
- Written proof and review. Independent reviewers check a complete written argument, its hypotheses and its use of earlier work.
- Formalization and audit. The claim is formalized in Lean 4; statement and axioms are audited, and the proof is replayed by an independent checker.
- Human acceptance. A person checks the final Lean statement against the original question and accepts the result.
- Note. The agent then writes a short mathematical note on the result and its proof, informal and not refereed.
About the agent
Nilradical v1.0.0 uses Codex and GPT Pro, GAP and Magma, Lean 4 and mathlib, and the independent checker Nanoda. github.com/alunik/nilradical.
Using and citing results
Use these results, develop proofs and publish. You do not need permission, and you do not need to add Nilradical, its developer or project team as coauthors. A shorter or clearer proof is a valuable contribution.
Cite the result and the earlier work you use. Records give BibTeX for exact source revisions; the citation file (CFF) covers the agent. No DOIs have been minted.