# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json version: "v0.4" # This metadata describes the current four-declaration Comparator checkpoint. # The selected final combined scope, including the supplied manuscript results, # is recorded in notes/BOONE_HIGMAN_PALOMAR_SELECTED_SCOPE.md. Update the theorem # list here together with the final challenge/solution and Comparator manifest # only when the corresponding closed Lean declarations exist. project: name: "Printed Questions around the Boone-Higman Conjecture, Stage 1" description: >- Answers to four printed open questions, stated in Mathlib's vocabulary and proved outright. First, an explicit finitely presented group containing every GL_n(Q): the Steinberg group St_10(R_L) of a six-generator, nine-relation ring R_L (Kourovka Notebook 14.10(c); Belk, Bleak, Matucci and Zaremsky, Problem 2.7). Second, Kohl's class transposition group CT(Z) is exactly the group of residue-class-wise affine permutations of Z that fix the nonnegative integers setwise (Kourovka Notebook 17.59). Third, for any two sets P1 and P2 of odd primes, Kohl's groups CT_P1(Z) and CT_P2(Z) generate CT_(P1 u P2)(Z), a negative answer to Kourovka Notebook 21.75. Fourth, Kohl's factorization conjecture: every residue-class-wise affine permutation of Z is a product of class shifts, class reflections and class transpositions (RCWA package manual, chapter 2). authors: [Sauers] responsible_maintainers: [SauersML] license: Apache-2.0 classification: arxiv: [math.GR, math.RA, math.KT] msc2020: ["20F05", "19C09", "20B07", "20H20"] sources: - title: Explicit finitely presented overgroups and class transposition groups type: original-proof relationship: other contributors: - name: Claude (Anthropic) role: developed the arguments, the Lean development and the prose of this submission under the user's direction note: >- The answers were found and written up in this repository under the user's direction. Their proofs are internal and have not had external expert review; bounded literature searches found no earlier answers, which is not a certification of priority. They rest on the work of others, notably the theory of Steinberg groups and Leavitt algebras and Kohl's theory of residue-class-wise affine groups. - title: Progress around the Boone-Higman Conjecture authors: [James Belk, Collin Bleak, Francesco Matucci, Matthew C. B. Zaremsky] year: 2023 type: paper id: https://arxiv.org/abs/2306.16356 location: Problem 2.7 (version 3) relationship: background note: >- Asks for an explicit finitely presented group containing GL_n(Q), the question answered by explicit_fp_overgroup_of_all_gl_n_q. - title: "Unsolved Problems in Group Theory. The Kourovka Notebook" authors: [E. I. Khukhro, V. D. Mazurov] year: 2026 type: paper id: https://arxiv.org/abs/1401.0300 location: Problems 14.10(c) (P. de la Harpe), 17.59 and 21.75 (S. Kohl) relationship: background note: >- Records Problem 14.10(c), an explicit finitely presented group containing GL_n(Q); Problem 17.59, whether CT(Z) is the group of residue-class-wise affine permutations fixing the nonnegative integers setwise; and Problem 21.75, whether CT_P1(Z) and CT_P2(Z) generate a proper subgroup of CT_(P1 u P2)(Z) when neither set contains the other. - title: "RCWA: Residue-Class-Wise Affine Groups (GAP package manual)" authors: [Stefan Kohl] type: other id: https://docs.gap-system.org/pkg/rcwa/doc/chap2.html location: Chapter 2 relationship: background note: >- States the conjecture that every residue-class-wise affine permutation of Z factors into class shifts, class reflections and class transpositions, and defines the three series. automation: methods: - method: agent models: [Claude (Anthropic)] framework: Claude Code tool_setup: >- AI-assisted mathematical exploration and Lean proof development, followed by submission preparation and remote verification. notes: >- Claude found and wrote up the arguments, produced the Lean development, and wrote the prose of this submission, under the user's direction. review: status: self-assessed notes: >- The arguments have had internal AI checks only; no human expert review or Palomar editorial acceptance is claimed. Internal status by theorem: Kourovka 14.10(c) and 21.75 and Kohl's factorization conjecture passed an internal referee; Kourovka 17.59 passed an adversarial check by a second lane. Verification for a selected revision is recorded in that revision's GitHub Actions runs. repository: role: substantive-development status: scope: >- A Lean 4 development over Mathlib, with a Comparator submission surface for the four theorems of Palomar/comparator-boone-higman.json. Palomar/BooneHigmanChallenge.lean states them in a Mathlib-only module carrying its own copies of the definitions they mention; Palomar/BooneHigmanSolution.lean proves them from the development. The rest of the repository is not offered as certified by this entry. main_results: - declaration: BooneHigman.explicit_fp_overgroup_of_all_gl_n_q file: Palomar/BooneHigmanSolution.lean comparator_config: Palomar/comparator-boone-higman.json - declaration: BooneHigman.kourovka_17_59 file: Palomar/BooneHigmanSolution.lean comparator_config: Palomar/comparator-boone-higman.json - declaration: BooneHigman.kourovka_21_75 file: Palomar/BooneHigmanSolution.lean comparator_config: Palomar/comparator-boone-higman.json - declaration: BooneHigman.kohl_factorization_conjecture file: Palomar/BooneHigmanSolution.lean comparator_config: Palomar/comparator-boone-higman.json fidelity: divergences: >- The ring R_L is the quotient of the free Z-algebra on six generators by the nine relations, as a RingQuot of FreeAlgebra. The Steinberg group is given by generators x_ij(r) with the standard relations, with x_ii(r) set to 1. Residue-class-wise affine permutations are rendered as permutations g of Z with a modulus m such that c g(n) = a n + b on each residue class, with c nonzero. Class transpositions, class shifts and class reflections are rendered by their action on the residue classes r + mZ with 0 <= r < m. In Kourovka 21.75 a set P of odd primes is a Set of natural numbers, CT_P(Z) is generated by the class transpositions whose two moduli have only prime factors in P together with 2, and the statement is for all pairs of sets, which contains the pairs of the printed question. Kohl's factorization conjecture is stated as the equality of the set of residue-class-wise affine permutations with the subgroup generated by the three series; the subgroup and the monoid they generate coincide, since the inverse of a class shift is its conjugate by the class reflection of the same class. acknowledgements: Built on Lean 4 and Mathlib; the mathematical sources are credited in sources.