Nilradical is a mathematical research agent. This site collects its results and Lean formalizations. The purpose is to support human mathematical work: understanding the ideas, finding connections and writing clear, illuminating proofs. These results are here for mathematicians to check, develop and publish, with credit for that work belonging to the people who do it.
Browse the workWord maps over ℂ and ℝ
Kourovka Notebook · 16.68Answer: Complex affirmative; real negativeNilradical v1.0.0
Every nonidentity two-variable word is surjective on PSL₂(ℂ). An explicit word of length 44 is not surjective on PSL₂(ℝ).
Complex proof and real counterexample by Nilradical v1.0.0. The complex argument uses work of Schneider–Thom and Mushkarov–Nikolov. The negative answer for SO₃(ℝ) is due to Andreas Thom.
Over ℂ
im w = PSL₂(ℂ)
Every nonidentity word in two variables is surjective.
Over ℝ
tr W(A, B) > 7/4
For an explicit word of length 44 and every A, B in SL₂(ℝ). Its projective word map is not surjective.
Work
Results and formalizations, with scope and sources. Citations and related work.
Word maps over ℂ and ℝ
Every nonidentity two-variable word is surjective on PSL₂(ℂ). An explicit word of length 44 is not surjective on PSL₂(ℝ).
The complex theorem extends to algebraically closed fields of characteristic zero. The compact case is prior work of Andreas Thom.
Soluble subgroups with trivially intersecting conjugates
In sufficiently large symmetric and alternating groups, any two soluble subgroups have conjugates that meet trivially.
One uniform eventual cutoff; the proposed threshold n ≥ 21 is not proved.
A p-nilpotency criterion for word values
A product-order condition on multilinear commutator values characterizes when the verbal subgroup of a finite group has a normal p-complement.
The Lean proof assumes two published structural theorems as explicit hypotheses.
An infinite subgroup with spread exactly one
In Thompson’s group F, the subgroup of maps with equal endpoint slopes is infinite and has spread exactly one.
Specializes Gili Golan-Polak’s generation theorem and assembles it with earlier fixed-point arguments; the required case is proved in Lean.
A dense two-generator subgroup of subexponential growth
Two explicit automorphisms of the rooted five-ary tree generate a dense subgroup of subexponential growth in the inverse limit of iterated wreath products of A₅.
Adapts Jérémie Brieussel’s sign-change method. The proof establishes the logarithmic growth limit, without an additional proposed explicit growth bound.
Preserving product orders 2 and 3 is not enough
A permutation of an involution class in a finite simple matrix group over GF(8) preserves product orders 2 and 3, but changes a product order from 5 to 7.
The recorded replay covers the endpoint’s complete dependency closure; it is not a fresh full-repository build.
A semiabelian group with a nonmonomial character
A semiabelian group of order 2592 has an irreducible complex character of degree 8 that is not induced from a linear character.
Uses Kida’s semiabelian complement; no minimal-order claim.
Cited by Meta AI in Semiabelian Groups Need Not Be Monomial ().
Reading the records
For an established theorem, the record credits its mathematical authors and Nilradical’s formalization contribution separately.
Proof sources and checks
Proof records identify the source, dependencies and any recorded checks, including their scope.
Statement review
Proof checks and human statement acceptance are recorded separately. Each record states its review status.
Mathematical notes
Notes explain the arguments and credit earlier work. Agent-written exposition is labelled and is not refereed.
Using the work
Check, develop and build on the work. Cite the original mathematics and any formalization you use. Records identify contributors and source revisions; Nilradical, its developer and the project team do not require coauthorship.
See a result citation