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.
Scope
Disproves universal conciseness for one-variable formulae, using actual first-order syntax and realization. The separate word-conciseness question 21.105 is outside scope.
Formal record
- Lean statement
- Kourovka/Problems/P21_106/Statement.lean
- Lean proof
- Kourovka/Problems/P21_106/Solution.lean
- Endpoint
- Kourovka.P21_106.not_notebookStatement
- Source commit
- 5a6b2c18e326b7b0281f00b64cade629acbfe1f5
- 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
- 16 September 2026, human statement verifier (acceptance record)
- Agent version
- Nilradical v0
Strict verification passed on 16 September 2026 for 7 endpoints: fresh compilation, frozen-statement comparison, a three-axiom policy, and checks by both Lean and Nanoda. Independent statement review passed. Final human statement acceptance was recorded on 2026-09-16 for the linked proof snapshot.
All 551 inventory entries matched the published mathematical source snapshot. Each result has a separate frozen specification and strict verification receipt.
Credit
Heisenberg counterexample, first-order encoding, proof and formalization by Nilradical v0.
- Nilradical v0 — discovery, proof and formalization
- Martina Conte and J. Moritz Petschick — original question
- 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 v0: solution and Lean proof of Kourovka Problem 21.106. Repository snapshot 5a6b2c18e326.
@misc{nilradical_v0_kourovka_21_106,
author = {{Nilradical}},
title = {Nilradical v0: solution and Lean proof of Kourovka Problem 21.106},
year = {2026},
howpublished = {Mathematical result with Lean formalization},
url = {https://github.com/alunik/kourovka-lean/blob/5a6b2c18e326b7b0281f00b64cade629acbfe1f5/Kourovka/Problems/P21_106/README.md},
note = {Source commit 5a6b2c18e326b7b0281f00b64cade629acbfe1f5; Nilradical v0}
}