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.
Scope
The complex theorem holds over every algebraically closed field of characteristic zero. The real construction is a nonidentity word of length 44 whose values on SL₂(ℝ) have trace greater than 7/4. Lean proves omission of a specified projective involution and nonsurjectivity on PSL₂(ℝ); omission of all nonidentity involutions is a written consequence of the trace bound. The negative SO₃(ℝ) answer is due to Andreas Thom and is not formalized in these projects.
Formal record
- Complex Lean statement
- Complex/WordMaps/Surjectivity.lean
- Complex Lean proof
- Complex/WordMaps/Surjectivity.lean
- Real Lean statement
- Real/RealWord/Counterexample.lean
- Real Lean proof
- Real/RealWord/Counterexample.lean
- Endpoints
- WordMaps.word_surjective
WordMaps.complex_word_surjective
RealWord.tr_value_gt_seven_fourths
RealWord.word_ne_one
RealWord.word_not_surjective
RealWord.exists_nontrivial_nonsurjective_word - Source commit
- 75b93ec1363f5ba4d138512a9dba13f749855f4e
- Verification
- Integrity passed (verification record)
- Statement review
- Independent review
- Novelty
- No earlier complete solution located in a bounded search (report); no priority claim is made
- Human acceptance
- 21 September 2026, human statement verifier (acceptance record)
- Agent version
- Nilradical v1.0.0; execution workflow 0.4.0-draft
Both frozen projects passed protected verification with statement comparison, the three-axiom policy, Lean and Nanoda. The complex run checked two declarations and the real run checked fifteen. No SO₃ proof or separate all-involution endpoint is included. Final human statement acceptance was recorded on 2026-09-21 for the linked proof snapshot.
All 23 accepted source and configuration files are preserved byte for byte in two standalone projects. The 21 September protected runs checked 2 complex and 15 real declarations with Lean and Nanoda. Publication retains those verification records and separately checks source identity and the public axiom audits.
Credit
Complex proof, explicit real counterexample and formalizations by Nilradical v1.0.0. The complex proof uses Schneider–Thom’s elementary-matrix specialization and a polynomial-fibre observation of Mushkarov–Nikolov. The compact answer is Thom’s prior result.
- Nilradical v1.0.0 — complex proof, real counterexample, formalization and verification
- J. Mycielski — problem proposer
- J. Schneider and A. Thom — elementary-matrix specialization
- O. Mushkarov and N. Nikolov — polynomial-fibre observation
- A. Thom — prior negative answer for SO₃(ℝ)
- Lean and mathlib contributors — formal foundations
Note
Read the mathematical note, an agent-written account of the result and its proof. It is informal and not refereed.
Cite
Nilradical. Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 16.68. Repository snapshot 75b93ec1363f.
@misc{nilradical_v1_0_0_kourovka_16_68,
author = {{Nilradical}},
title = {Nilradical v1.0.0: solution and Lean proof of Kourovka Problem 16.68},
year = {2026},
howpublished = {Mathematical result with Lean formalization},
url = {https://github.com/alunik/kourovka-lean/blob/d677596183f8c4ac538d692ab03c80005d1f15d5/Kourovka/Problem1668/README.md},
note = {Source commit 75b93ec1363f5ba4d138512a9dba13f749855f4e; Nilradical v1.0.0}
}