{"id":"37849755-09e6-47c4-8764-75833de7ec72","arxiv_id":"2501.09769","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A Lean formalization proves that every group of order pq (p and q prime) is cyclic or one of the known noncyclic semidirect or direct product groups.","lead":"This paper reports a machine-checked proof in the Lean theorem prover of the classical classification of groups of order p times q, for prime numbers p and q. It also formalizes the internal direct and semidirect product characterizations that the proof relies on.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant mathematical objection identified: the formal statements match Theorem 2.1 and the proof dependencies are standard. Residual risk is only that the linked Lean code is unpinned and was not independently compiled, so the formalization claim rests on repository trust.","rationale":"The paper's central formalisation claim is mathematically credible and internally consistent. The displayed statements in Figure 1 correspond exactly to the natural-language classification: existence of a noncyclic group is characterised by p = q or p | q − 1 or q | p − 1, and any two noncyclic groups of the same prime-multiplicative order are isomorphic. The p < q semidirect-product theorems correctly use C_q as the normal factor, and the statement parametrised by an arbitrary nontrivial φ correctly encodes uniqueness of the nonabelian isomorphism class, relying on cyclicity of Aut(C_q). The internal semidirect-product characterisation in Figure 2 has the correct hypotheses (normal subgroup, intersection bottom, join top, conjugation-induced action). I found no circularity and no mismatch that would make the formal theorems express a different mathematical statement. The reader's weakest-assumption remark about mathlib definitions and dependencies is reasonable but speculative; it points to the standard way all Lean formalisations depend on the library. The only concrete, testable gap is that the linked repository is not pinned to a mathlib commit and no axioms output is shown, so an independent reader cannot verify from the paper alone that the code compiles and is sorry-free. This is a standard reproducibility concern for formalisation papers and does not warrant changing the reader's ACCEPT verdict; running the proposed build-and-#print-axioms check would settle it.","tokens_in":7426,"tokens_out":19144,"duration_ms":198823,"concrete_test":"Checkout https://github.com/wupr/order-p-q, pin the exact mathlib commit from its lean-toolchain/lake-manifest.json, run lake build, then run #print axioms on the five theorem names in Figure 1 (exists_card_eq_prime_mul_prime_and_not_isCyclic_iff, nonempty_mulEquiv_of_card_eq_prime_mul_prime_of_not_isCyclic, nonempty_mulEquiv_prod_of_card_eq_prime_pow_two_of_not_isCyclic, nonempty_mulEquiv_semidirectProduct_of_card_eq_prime_mul_prime, nonempty_mulEquiv_semidirectProduct_of_card_eq_prime_mul_prime_of_not_isCyclic); confirm the output contains no sorry and no unexpected axioms beyond standard Classical.choice/Quot.sound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I read the paper in good faith and looked for a place where the central claim—that the classification of groups of order pq is formalised in Lean—could fail. The five displayed theorems are faithful transcriptions of Theorem 2.1: the existence criterion includes p = q and both divisibility alternatives; the uniqueness theorem covers all noncyclic groups of order pq, including p = q; the semidirect-product theorems use the correct normal factor C_q and action φ : C_p → Aut(C_q), with the arbitrary-nontrivial-φ statement faithful to the classic fact that all nontrivial homomorphisms give isomorphic groups. The proof dependencies cited (Sylow theory, internal semidirect/direct product characterisations, and cyclicity of the unit group of a finite integral domain) are standard mathlib material, and I found no circular use of the classification being proved. The one genuine residual risk is not mathematical: the repository is linked but no mathlib commit is pinned, and the paper does not display #print axioms output or a build log. If the code at the linked repository does not compile against a current mathlib, or contains sorries, the formalisation claim would not hold. This is a verification/reproducibility caveat, not an identified flaw in the argument, and it does not by itself undermine the plausibility of the reported formalisation.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports a Lean formalisation of the classification of groups of order p q for primes p and q, not necessarily distinct. The main formal theorems, displayed in Figure 1, express the existence and uniqueness up to isomorphism of noncyclic groups of order p q, the structure of noncyclic groups of order p^2 as C_p × C_p, and the semidirect-product description for p < q. The paper also formalises the internal characterisations of direct and semidirect products (Figure 2) and discusses implementation choices: the concrete cyclic group MulZMod, the use of Nat.card and Finite instead of Fintype, design choices in stating classification results, the semidirect-product API, and the proof that Aut(C_p) is cyclic of order p−1 via ZMod ring theory. The Lean code is available at the linked repository [8].","tokens_in":7667,"tokens_out":7836,"duration_ms":79223,"significance":"If the linked code compiles, this is a useful, machine-checked addition to mathlib's finite group theory coverage. The formal statements in Figure 1 appear faithful to Theorem 2.1, including the p = q case and the divisibility conditions, and the proof dependencies (Sylow theory, internal product characterisations, cyclicity of the unit group of a finite integral domain) are standard. There is no circular use of the classification being proved. The paper is also transparent about formal choices such as multiplicative ZMod representatives and the use of Nonempty isomorphism statements. The main residual concern, that the repository is unpinned and was not independently compiled, is a reproducibility caveat rather than an identified mathematical flaw; I did not recompile the code myself.","major_comments":[],"minor_comments":[{"comment":"The sentence 'a semidirect product Cq ⋊φ Cp depends on a choice of homomorphism φ : Cq → Aut(Cp)' swaps the domain and codomain; it should be φ : Cp → Aut(Cq), since Cq is the normal factor. The subsequent existence condition 'p | q−1' is consistent with the corrected direction, and the proof outline later states the correct direction, so this is a typo rather than a mathematical error.","section":"Section 2, paragraph after Theorem 2.1"},{"comment":"For reproducibility, please state the Lean version and a pinned mathlib commit at which the development compiles, and ideally include the output of `#print axioms` for the five main theorems. The current text says the imports can be found in the source code, but without a pinned commit the reader cannot independently reconstruct the exact environment.","section":"Section 3, first paragraph and reference [8]"},{"comment":"There is a typo: 'Mulplicative' should be 'Multiplicative'. Similar typographical issues ('efficient', 'sufficient') appear in Section 4.3.","section":"Section 4.1"},{"comment":"The statement of `mulEquivProd` is correct, but it would be helpful for the caption to note explicitly that the direct-product characterisation is derived from the semidirect-product one via the trivial action; the prose says this, but a one-sentence reference in the caption would aid readability.","section":"Figure 2"}],"recommendation":"accept","confidential_remarks":"I did not independently compile the linked repository, so my assessment assumes the displayed statements are accurate transcriptions of the code and that the repository contains no sorries. If the editors wish to enforce stronger reproducibility standards, requesting a pinned mathlib commit would be a sufficient remedy; I see no mathematical issue that would require further review."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does what it says: it reports a machine-checked Lean formalization of the classification of groups of order pq, and the displayed statements match Theorem 2.1 faithfully, including the p = q case and the subtle 'the semidirect product' shorthand. The genuinely new and useful part is not the mathematics—that is standard textbook material—but the reusable characterizations of internal direct and semidirect products (mulEquivSemidirectProduct and mulEquivProd), which will likely help future formalization projects in group theory. The proof strategy is sound: Sylow theory, the internal product characterizations, and the standard mathlib result that the unit group of a finite integral domain is cyclic. I found no sign of circularity; the classification is not assumed anywhere, and the dependencies are reasonable.\n\nThe weak spots are minor but real. The paper does not pin a mathlib commit, does not show a build log, and does not print axioms, so the formalization claim rests on trusting the linked repository. That is a reproducibility caveat, not a flaw in the argument—the code is linked, it is being integrated into mathlib, and the statements in the paper give enough detail that a motivated referee can verify. I also note a couple of harmless typos (e.g., 'Mulplicative'), which do not affect the content.\n\nThe paper is honestly framed: it explicitly says the theorem is classical and the contribution is the Lean coverage. It cites relevant prior work (prime order and order four formalizations). The authors do not overclaim. For a Lean/mathlib audience, this fills a clear gap and provides reusable infrastructure. For a general mathematics audience, the value is mostly as a demonstration of formalization practice.\n\nI recommend sending this to peer review. A serious referee should check that the repository compiles against the stated mathlib version and that the five theorem statements indeed correspond to the informal classification. That is doable and worthwhile. The paper is short, readable, and honest about its scope.","headline":"A clean, credible formalization note: the math is textbook, the reusable Lean lemmas are the real contribution, and the only real caveat is reproducibility hygiene (no pinned mathlib commit).","tokens_in":8149,"tokens_out":1031,"would_cite":false,"duration_ms":12702,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["20D60","20E22","68V20"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes in the Lean theorem prover a machine-checked classification of all groups of order $p q$ for prime numbers $p$ and $q$.","keywords":["groups of order pq","classification of finite groups","Lean theorem prover","machine-checked proof","semidirect products","cyclic groups","internal direct products","formal mathematics"],"falsifier":"Open the linked Lean repository and check that the five declarations in Figure 1 are accepted by the Lean kernel with no `axiom`, `sorry`, or `admit` among their dependencies; if any such gap appears, or if the statements differ from Figure 1, the claim of a machine-checked classification is not established.","tokens_in":7223,"feed_emoji":"✅","tokens_out":8634,"duration_ms":76115,"temperature":0.7,"pith_summary":"The paper's main claim is that the classical classification of groups of order $p q$, for prime numbers $p$ and $q$, can be stated and proved inside the Lean theorem prover. The formal development covers both the case $p = q$ and the case $p \\neq q$, and it records five theorem statements that together say exactly when a noncyclic group of order $p q$ exists, what it looks like, and why it is unique up to isomorphism. Along the way the authors formalise a general characterisation of internal direct and semidirect products, which they expect to be reusable in later formalisations. If the formalisation is correct, then a computer-checked proof of this classification is available, not just a human-written one.","feed_headline":"Lean proof classifies all groups of order p×q","feed_subtitle":"Every group of order p×q is cyclic, a direct product, or a semidirect product, and the computer has verified it.","key_machinery":"The machine-checked proof is carried by the internal semidirect product characterisation `mulEquivSemidirectProduct`, which turns the subgroup conditions $N \\sqcap H = \\bot$ and $N \\sqcup H = \\top$ into an explicit isomorphism $G \\cong N \\rtimes_\\varphi H$ with $\\varphi$ the conjugation action restricted to $H$, together with its direct-product counterpart `mulEquivProd`. To give a concrete target for the classification, the paper defines `MulZMod n`, the multiplicative version of the additive group `ZMod n`, as a cyclic group of order $n$, and states the noncyclic groups of order $p q$ as `MulZMod q ⋊[φ] MulZMod p`. A key mathematical input is that $\\operatorname{Aut}(C_p) \\cong C_{p-1}$, obtained by identifying the automorphism group of `ZMod p` with the unit group of the finite integral domain `ZMod p` and using the cyclicity of that unit group.","core_discovery":"The central claim is that a finite group $G$ with $|G| = p q$, where $p$ and $q$ are prime, is cyclic unless $p = q$ or one of $p, q$ divides one less than the other. In the noncyclic case $G$ is isomorphic either to $C_p \\times C_p$ (when $p = q$) or to the semidirect product $C_q \\rtimes C_p$ (when $p < q$ and $p \\mid q-1$), and any two such noncyclic groups are isomorphic. The paper packages this as five explicit Lean theorems, including the iff statement `exists_card_eq_prime_mul_prime_and_not_isCyclic_iff` and the uniqueness statement `nonempty_mulEquiv_of_card_eq_prime_mul_prime_of_not_isCyclic`. It also formalises Lemma 2.2: if subgroups $N, H \\le G$ satisfy $HN = G$ and $H \\cap N = 1$, with $N$ normal, then $G$ is isomorphic to the semidirect product $N \\rtimes_\\varphi H$, and if both subgroups are normal then $G \\cong H \\times N$.","pith_inferences":["The same internal semidirect product characterisation is a natural building block for the next classifications, such as groups of order $p^3$ or $p^2 q$, where the same subgroup-complement pattern recurs.","The decision to work with `MulZMod` as a concrete multiplicative representative of $C_n$ suggests a template for stating future classification theorems as explicit isomorphisms to named models, rather than only as existential statements.","If the classification is absorbed into the library, then any later formal proof involving groups of order $p q$ can rely on it; the main fragility would be that a future refactor of the unit-group cyclicity theorems would force rechecking the proof's dependency chain."],"forward_implications":["The formal iff theorem gives a complete existence criterion: a noncyclic group of order $p q$ exists exactly when $p = q$, $p \\mid q - 1$, or $q \\mid p - 1$.","Because the statements are uniform in $p$ and $q$, the classification of groups of order $p^2$ is included as the special case $p = q$.","The reusable `mulEquivSemidirectProduct` and `mulEquivProd` lemmas provide a standard route for proving that a group with two complementary subgroups is a semidirect or direct product, which is the central structural step of the proof.","The uniqueness theorem asserts that any two noncyclic groups of order $p q$ are isomorphic, so mathematicians can speak of 'the' noncyclic group of order $p q$ whenever one exists.","The code, once incorporated into the library, gives later formalisation projects a certified classification statement to cite instead of reproving the classification."],"supporting_citations":[{"why":"It describes the Lean theorem prover, the system in which the formalisation is written and checked.","marker":"[3]"},{"why":"It is the OrderPQ repository containing the full Lean code for the formalisation and the five main theorem statements.","marker":"[8]"},{"why":"It is the mathlib library that supplies the group theory definitions, the ZMod and semidirect product constructions, and the unit-group cyclicity theorems used in Section 4.5.","marker":"[10]"}],"fun_headline_variants":["Lean verifies classification of groups of order p×q","Formal proof: groups of order pq classified","All order-pq groups classified in Lean","Lean proof: every order-pq group is classified","Computer-checked proof: order-pq groups classified"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The formal proof inherits the correctness of the existing library it imports, especially the facts that the unit group of a finite integral domain is cyclic and that the unit group of `ZMod p` has size $p-1$, along with the library's encoding of groups, subgroups, and semidirect products.","fun_headline_variants_meta":{"raw":{"variants":["Lean verifies classification of groups of order p×q","Formal proof: groups of order pq classified","All order-pq groups classified in Lean","Lean proof: every order-pq group is classified","Computer-checked proof: order-pq groups classified"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001011,"raw_usage":{"total_tokens":4211,"prompt_tokens":826,"completion_tokens":3385,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":442,"completion_tokens_details":{"reasoning_tokens":3311}},"tokens_in":442,"tokens_out":3385,"duration_ms":24719,"temperature":1.0,"reasoning_tokens":3311,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T19:52:42.727161+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Open the linked Lean repository and check that the five declarations in Figure 1 are accepted by the Lean kernel with no `axiom`, `sorry`, or `admit` among their dependencies; if any such gap appears, or if the statements differ from Figure 1, the claim of a machine-checked classification is not established.","supporting_citations":[{"cited_title":"de Moura, S","cited_arxiv_id":null,"evidence_quote":"It describes the Lean theorem prover, the system in which the formalisation is written and checked."},{"cited_title":"Harper and P","cited_arxiv_id":null,"evidence_quote":"It is the OrderPQ repository containing the full Lean code for the formalisation and the five main theorem statements."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"It is the mathlib library that supplies the group theory definitions, the ZMod and semidirect product constructions, and the unit-group cyclicity theorems used in Section 4.5."}],"review_version":1}