{"id":"97848bbd-e93f-4212-8efc-8efe9676c457","arxiv_id":"2607.17477","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Eight open Kourovka Notebook problems are resolved by explicit constructions and counterexamples, with proofs claimed to be formally verified in Lean.","lead":"This paper reports machine-checked solutions to eight open problems in group theory from the Kourovka Notebook, mostly explicit constructions and counterexamples. A generalist should look because it is an early demonstration of an automated reasoning agent discovering and formally verifying new mathematics, not just checking known proofs.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2.1's printed proof has a subscript error: the u_i/v_i definitions and the exponent '2i' are inconsistent, breaking the derived-series induction unless corrected to 2^i. The Lean artifact must be audited to confirm the theorem.","rationale":"I read the paper in good faith and spot-checked multiple sections. Sections 3, 4, 5, 7, 8, and 9 appear mathematically sound: the permuted-product construction checks, the order/totient-sum tables in Section 4 are internally consistent, the Rota-Baxter verification is correct, the cograph/chordal argument is valid, the Heisenberg counterexample works, and the p-group rank counterexample is correct. The reader's weakest_assumption focused on the unshown finite computations and the unpinned Lean artifact. I partially agree: those are real auditability concerns. However, the single most concrete load-bearing issue is in Section 2, where the printed definitions of u_i and v_i and the exponent '2i' make the central induction of Theorem 2.1 incoherent. This is more specific than the general 'trust the computations' concern, and it directly affects one of the eight stated solutions. Because the theorem may still be correct and the Lean proof, if present, would settle it, I do not think the overall verdict should change from CONDITIONAL; it remains conditional on obtaining and auditing the formal artifact and correcting the prose. Hence verdict_should_be is UNCHANGED relative to the reader's verdict.","tokens_in":24176,"tokens_out":33178,"duration_ms":247936,"concrete_test":"Pin the GitHub repository in footnote 1 to a specific commit, run `lake build` (or the project's build command), and inspect the formal Lean proof of Theorem 2.1 to verify whether it defines u_i and v_i with exponents 2^i (equivalently, whether the formal proof of the derived-series induction matches the corrected reading). If the Lean theorem compiles and the formal definitions align with the corrected notation, the concern is settled. If the repository cannot be built or the formal proof is absent, the paper's central verification claim is not auditable.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central proof of Section 2, Theorem 2.1, is not self-contained as printed. The text defines u_i := e_{m0,m0+2i} and v_i := e_{m0+2i,m0+2i+1}, and claims g^{2i} u_i g^{-2i} = v_i and u_{i+1} = [u_i, v_i]. With these definitions, the identities fail for i ≥ 1. For example, u_1 = e_{m0,m0+2}, so g^2 u_1 g^{-2} = e_{m0+2,m0+4}, which is not v_1 = e_{m0+2,m0+3}. Moreover, the displayed computation of [u_0,[u_0,g]] uses v_0 = e_{m0+1,m0+2}, whereas the printed v_i definition at i=0 gives e_{m0,m0+1}. The argument only works if the intended definitions are u_i = e_{m0,m0+2^i}, v_i = e_{m0+2^i,m0+2^{i+1}}, and conjugation by g^{2^i}; the superscripts appear to have been lost in typesetting or editing. Thus one of the eight headline theorems rests on an informal proof that cannot be followed as written, pushing the reader to the Lean repository, which is linked but has no commit hash. This is not a dispute with the underlying mathematics—the corrected induction is plausible—but it is a load-bearing gap in the paper's claim to provide readable natural-language solutions.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents solutions to eight open problems from the Kourovka Notebook, one dating back to 1969. The results are: a group with exactly two maximal locally soluble normal subgroups (Theorem 2.1); groups whose n! permuted products take exactly k values for every 1 ≤ k ≤ n! (Theorem 3.1); two groups of order 6048 with equal totient sums but only one simple (Theorem 4.1); a surjective non-injective Rota–Baxter operator on a non-abelian group (Theorem 5.1); identification of the group generated by horizontal class transpositions of modulus at most k with S_lcm(2,...,k) (Theorem 6.1); cograph power graphs of finite groups are chordal (Theorem 7.1); right-relatively convex subgroups need not form a sublattice (Theorem 8.1); and a counterexample to a proposed rank inequality for p-group extensions (Theorem 9.1). Each proof is accompanied by a claim of formal verification in Lean by the Aristotle agent, and an appendix describes the formalization workflow.","tokens_in":24571,"tokens_out":27111,"duration_ms":227788,"significance":"If the results are correct, the paper resolves eight problems from a standard open-problem collection in group theory, including one of long standing. The constructions are explicit and the statements are falsifiable; several results have already been independently obtained by other researchers (e.g., Pan for Theorem 6.1, Rundström for Theorem 7.1), which increases confidence. The strongest feature is the claim that every proof is machine-checked in Lean, and the paper is transparent about the human-AI division of labor. However, the manuscript is not fully self-contained in a few places: the proof of Theorem 2.1 contains a notational error that invalidates the printed induction, and the base case of Theorem 6.1 is delegated to an unshown computation. These issues are local and fixable, but they are load-bearing for the corresponding theorems.","major_comments":[{"comment":"The definitions of u_i and v_i are incompatible with the displayed identities. The text defines u_i := e_{m0,m0+2i} and v_i := e_{m0+2i,m0+2i+1}. With these definitions, g^{2i} u_i g^{-2i} = e_{m0+2i,m0+4i}, which equals v_i only for i = 0, and [u_i, v_i] = e_{m0,m0+2i+1}, not u_{i+1} = e_{m0,m0+2i+2}. Moreover, the displayed computation of [u_0,[u_0,g]] uses v_0 = e_{m0+1,m0+2}, whereas the printed definition gives v_0 = e_{m0,m0+1}. The intended definitions are clearly u_i = e_{m0,m0+2^i}, v_i = e_{m0+2^i,m0+2^{i+1}}, with conjugation by g^{2^i}. As printed, the induction proving that the derived subgroups of H are nontrivial cannot be followed. This is a load-bearing error for Theorem 2.1, though it is easily corrected; the Lean file should be checked against the corrected statement.","section":"Section 2, paragraph after Lemma 2.5"},{"comment":"The proof that CT(4) = S_12 rests on the assertion (σ^(3)_{0,1} σ^(4)_{0,1})^3 = (6 7) and on eleven displayed conjugation identities, followed by “These identities can all be verified computationally.” No calculation or derivation is provided. Because these identities supply the entire base case of the induction, the natural-language proof is not self-contained: the reader must either rerun the computation or trust the claimed Lean formalization. I recommend adding the computation in an appendix or giving a precise pointer to the verified Lean code, and pinning the repository version.","section":"Section 6, base case of Theorem 6.1"},{"comment":"The element-order distribution of PSU(3,3) is stated as a table with no derivation. The totient sum 23984 depends exactly on this table, and the same is true for the distribution of H in Lemma 4.3. These are finite computations and may be routine, but since Theorem 4.1 is a counterexample based on these numerical coincidences, the text should at least indicate how the distributions were obtained (for instance, from conjugacy classes of PSU(3,3) or from the cited ATLAS file) or refer to a checked computation in the Lean repository.","section":"Section 4, Lemma 4.2"}],"minor_comments":[{"comment":"The trichotomy “one of g_1, g_1 g_2, g_1^2 g_2 must have both translation coordinates nonzero” is unnecessary: if g_1 has nonzero first coordinate and g_2 has nonzero second coordinate, then g_1 g_2 already has both translation coordinates nonzero. This is not an error in the argument, but the wording is confusing.","section":"Section 2, sentence before Lemma 2.5"},{"comment":"Some displayed conjugation identities have unbalanced parentheses due to the line-breaking (for example, the display for (0 1)). This makes the formulas harder to check. Please reformat them.","section":"Section 6, displayed formulas"},{"comment":"The repository is cited by URL only, with no commit hash. Since the paper’s formal-verification claim is central, a pinned hash is essential for reproducibility and for refereeing the Lean code.","section":"Appendix A / GitHub link"},{"comment":"In the proof of convexity of H_1, the step “it follows that c_y = 0” is compressed. A sentence explaining that both c-a and b-c must lie in the positive cone P is enough; currently the reader has to supply the case analysis.","section":"Section 8"}],"recommendation":"major_revision","confidential_remarks":"The mathematical core appears sound: I spot-checked the central-extension cocycle in Section 3, the Rota–Baxter equation in Section 5, the induced-P4 argument in Section 7, and the commutator computations in Section 9, and found no errors. The Section 2 problem is almost certainly a typographical loss of superscripts (2^i instead of 2i), but as printed it is a genuine gap in the proof of one of the headline theorems. I would ask the authors to correct that argument, supply the missing base-case computation for Theorem 6.1 or a precise Lean reference, and pin the repository hash. The AI-discovery narrative is disclosed transparently and is outside my mathematical assessment."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's my take. The paper makes eight genuine contributions: eight open Kourovka problems get solutions, with Lean formal verification behind them. The construction in Section 3 (central extension with inversion code) is particularly neat, and Section 7's proof that cograph power graphs are chordal is a clean argument. The authors also credit independent work by Pan and Rundström where it exists, and the citation practice is honest. On spot-checking, the math in Sections 3–9 holds together.\n\nThe soft spot is Theorem 2.1. The printed proof has a subscript error that breaks the induction. The text defines u_i := e_{m0,m0+2i} and v_i := e_{m0+2i,m0+2i+1}, then claims g^{2i} u_i g^{-2i} = v_i. With these definitions the identity fails: for i=1, g^2 u_1 g^{-2} = e_{m0+2,m0+4}, while v_1 = e_{m0+2,m0+3}. The computation of [u0,[u0,g]] also uses v_0 = e_{m0+1,m0+2}, which is not the printed v_0. The intended definitions are almost certainly u_i = e_{m0,m0+2^i}, v_i = e_{m0+2^i,m0+2^{i+1}}, with conjugation by g^{2^i}. As written, the natural-language proof of one of the eight headline theorems cannot be followed. This is fixable, but it's not a cosmetic detail; the paper explicitly promises readable informal proofs alongside the machine-checked ones. The Lean repository should be pinned to a commit hash so the formal proof can be checked.\n\nI also think the abstract oversells the 'autonomously discovered' phrase. Appendix A is more careful: humans selected problems, wrote formal statements, split proofs into lemmas, and prompted for partial progress. That is a real workflow, but it is not autonomous in the usual sense. The appendix deserves to be the source of truth; the abstract should match it.\n\nMinor point: Section 6's base-case identities and Section 4's order distributions are asserted as 'verified computationally' without reproduction. That is acceptable in principle, but it puts the burden on the Lean artifact, which brings us back to the commit-hash issue.\n\nOverall: the mathematical claims look sound, the soft spots are presentation and auditability, not hidden circularity. The paper is worth a serious referee. Send it out, but require the Theorem 2.1 fix and a pinned repository.","headline":"Eight real solutions to Kourovka problems, Lean-backed, but Theorem 2.1's printed proof has a subscript error that must be fixed before the paper works as a readable informal account.","tokens_in":25023,"tokens_out":6801,"would_cite":true,"duration_ms":59452,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68V20","05C25","05E16","06F15","17B38","20B30","20D06","20D15"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper resolves eight open problems from the Kourovka Notebook, offering explicit constructions and counterexamples, and reports that every proof is verified by a computer.","keywords":["Kourovka Notebook","group theory","locally soluble groups","permuted products","Rota-Baxter operators","class transpositions","power graphs","formal verification"],"falsifier":"Independently recompute the element-order distributions of PSU(3,3), C6×S4×F, and C2×W×F and verify that each has total sum 6048 and totient sum 23984; a mismatch would refute Theorem 4.1. Alternatively, recompute the twelve conjugation identities in Section 6 to confirm that (σ(3)_{0,1}σ(4)_{0,1})^3 = (6 7); if that equation fails, the induction proving CT(k) ≅ S_{lcm(2,...,k)} collapses.","tokens_in":24091,"feed_emoji":"🧮","tokens_out":14287,"duration_ms":119033,"temperature":0.7,"pith_summary":"The paper reports solutions to eight open problems from the Kourovka Notebook, a standard collection of open questions in group theory. The answers are explicit constructions or counterexamples: a group with exactly two maximal locally soluble normal subgroups; for each 1 ≤ k ≤ n! a group whose n! ordered products of n chosen elements take exactly k values; a simple and a non-simple group with the same order and same totient sum; a surjective but non-injective Rota–Baxter operator on a non-abelian group; the identification of a class-transposition group with a finite symmetric group; the statement that cograph power graphs are chordal; right-relatively convex subgroups that do not form a sublattice; and a p-group extension where a natural rank inequality fails. The paper also reports that every proof was developed and checked by an automated formal reasoning system, so the results come with machine-verified formalizations.","feed_headline":"Eight open problems in group theory solved, with machine-checked proofs","feed_subtitle":"The answers cover new constructions and counterexamples, and each proof is verified step by step by a computer.","key_machinery":"The constructions differ by section. The permuted-products theorem is carried by a central extension Z^n × Z/kZ whose multiplication has the bilinear factor B(u,v)=Σ_{i<j} u_j v_i (j−1)! mod k; this turns the inversion vector of a permutation into a single residue. The local-solubility result uses a semidirect product of unipotent matrices over Z² with lattice translations, with a commutator estimate showing [U_d,U_e]≤U_{d+e}. The simplicity pair uses the group PSU(3,3) acting primitively on 28 isotropic points. The class-transposition theorem uses a standard theorem on primitive permutation groups containing a 3-cycle. The cograph/chordal proof uses a cyclic-subgroup containment dichotomy;","core_discovery":"The paper claims to settle all eight open problems, each with a machine-checked proof. The results are explicit: a group with exactly two maximal locally soluble normal subgroups; for every 1 ≤ k ≤ n! a group whose n! ordered products of n chosen elements take exactly k values; groups of order 6048 and equal totient sum 23984 with different simplicity; a surjective non-injective Rota–Baxter operator on a non-abelian group; CT(k) ≅ S_{lcm(2,...,k)}; cograph power graphs are chordal; right-relatively convex subgroups need not form a sublattice; and a p-group extension in which rank(Z(H)∩H′) exceeds rank(B).","pith_inferences":["The inversion-vector central extension used for permuted products suggests a general recipe: any statistic on permutations that can be computed as a sum of fixed weights can be forced to take exactly k values by working modulo k. One could test whether the same construction works for other natural statistics, such as total displacement rather than inversion count.","The class-transposition theorem gives an explicit generation of every permutation of {0,...,lcm(2,...,k)-1} by modulus-bounded transpositions; a practical consequence would be an algorithm that decomposes any such permutation as a product of class transpositions, with possible use in computing with maps on residue classes that iterate affine steps.","The counterexample to the rank inequality has p=3, rank(B)=2 and rank(Z(H)∩H′)=3; an obvious next step is to determine, for each prime p, the largest possible gap between these ranks, or whether a rank-1 counterexample exists.","The workflow described in the paper — automated formal search producing a human-readable proof after verification — could be applied to other open problems whose answers are finite constructions. The main caveat, tied to the paper's own lack of reproduced computations, is that such a workflow needs its computational checks to be independently rerunnable."],"forward_implications":["Every value 1 ≤ k ≤ n! occurs as the number of distinct products obtained by permuting n elements in some group.","Order and totient sum together do not characterize simplicity: PSU(3,3) and a non-simple group of order 6048 share the same totient sum 23984.","The group generated by horizontal class transpositions with modulus at most k is the full symmetric group on lcm(2,...,k) elements for every k ≥ 4.","A finite group whose power graph is a cograph has a chordal power graph.","In extensions of elementary abelian p-groups, the rank of Z(H)∩H′ can exceed the rank of B, so the proposed rank bound is false."],"fun_headline_variants":["Eight open group theory problems solved, all proofs machine-checked","Kourovka Notebook: eight problems solved with formal proof","Computer-verified answers to eight group theory challenges","Autonomous agent cracks eight Kourovka problems","New constructions and counterexamples: eight problems solved"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The results stand on finite checks that the paper does not reproduce — twelve conjugation identities in the proof of Theorem 6.1, the element-order distributions in Section 4, and machine-checked proof files whose exact version is not given — so any undetected error in these checks would undo the corresponding theorem.","fun_headline_variants_meta":{"raw":{"variants":["Eight open group theory problems solved, all proofs machine-checked","Kourovka Notebook: eight problems solved with formal proof","Computer-verified answers to eight group theory challenges","Autonomous agent cracks eight Kourovka problems","New constructions and counterexamples: eight problems solved"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000943,"raw_usage":{"total_tokens":3864,"prompt_tokens":738,"completion_tokens":3126,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":482,"completion_tokens_details":{"reasoning_tokens":3063}},"tokens_in":482,"tokens_out":3126,"duration_ms":18114,"temperature":1.0,"reasoning_tokens":3063,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T17:51:58.669921+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Independently recompute the element-order distributions of PSU(3,3), C6×S4×F, and C2×W×F and verify that each has total sum 6048 and totient sum 23984; a mismatch would refute Theorem 4.1. Alternatively, recompute the twelve conjugation identities in Section 6 to confirm that (σ(3)_{0,1}σ(4)_{0,1})^3 = (6 7); if that equation fails, the induction proving CT(k) ≅ S_{lcm(2,...,k)} collapses.","supporting_citations":[],"review_version":1}