Pith. sign in

REVIEW 3 major objections 4 minor 33 references

Mining Math Conjectures from LLMs: A Pruning Approach

T0 review · 3 major / 4 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read LLMs paired with a computational checker can produce original but simple math conjectures, though they often fail to write runnable code.

desk verdict A modest, honest study of LLM-generated conjectures on the solubilizer, but the 'no counterexample' label overstates the search coverage. read the letter →

arxiv 2412.16177 v1 pith:JBGUH7XI submitted 2024-12-09 cs.AI

Jake Chuharski , Elias Rojas Collins , Mark Meringolo This is my paper · ORCID
classification cs.AI MSC 20D1020D6068T50
keywords LLMconjecturegenerationsolubilizerfinitegrouptheoryGAPcomputeralgebracounterexamplepruningautomatedmathematicaldiscoveryguess-and-checkpipelineChatGPTGeminiClaude
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish a modest empirical point: large language models can generate original mathematical conjectures in a specialized, unfamiliar area if each conjecture is immediately checked by computational algebra. Focusing on the solubilizer—the set of elements that generate a solvable subgroup together with a given element—the authors run a generate-and-prune loop in which ChatGPT, Gemini, and Claude propose conjectures, write GAP code to test them, and any falsified conjecture is fed back into the prompt. Of 420 unique outputs, 40 withstood the counterexample search and 109 were falsified by code that ran; the rest failed because the generated code did not execute. The upshot is that LLMs can act as a plausible brush-clearing tool for new mathematical constructs, even though they lean on known ideas and cannot yet be expected to produce major new mathematics.

What carries the argument

The object is the solubilizer, $\operatorname{Sol}_G(x) = \{y \in G \mid \langle x, y\rangle \text{ is solvable}\}$, a set that is not generally a subgroup. The method is a generate-and-prune loop: the LLM receives the definition, true results from the literature, and the current list of falsified conjectures; it outputs a conjecture plus GAP code; the code is executed; if it finds a counterexample, that conjecture is added to the prompt's false list and the loop repeats. This guess-and-check machinery lets the model's creativity be filtered by computation without a theorem prover, and the deliberately obscure subject reduces the chance that the model is regurgitating training data.

What would settle it

Take the surviving conjectures—for instance Conjecture 4.1 or Conjecture A.1—and run the same GAP search over all non-solvable groups of order up to 1,000,000, not just the simple ones, then extend beyond that bound; a single counterexample would show the 'No Counter-examples' label was an artifact of the restricted search space rather than evidence of plausibility.

Watch

Extended reading notes

Core claim

The central discovery is that a generic LLM, given the definition of a relatively recent group-theoretic object and some literature, can produce conjectures that are distinct from the prompt material and that survive a computational counterexample search—provided the search is implemented as a loop rather than a one-shot generation. The paper reports that 40 of 420 unique conjectures returned 'No Counter-examples' under GAP checks on groups up to order 1,000,000, while 109 were refuted by concrete counterexamples and 271 could not be tested because the model's code did not run. The authors argue this shows LLMs are capable of original, simple conjecture generation, with ChatGPT producing the most surviving conjectures and OpenAI o1, in a small auxiliary sample, producing executable code far more often. The claim is deliberately modest: the value is the pipeline, not any single conjecture.

Load-bearing premise

The claim that a conjecture is plausible rests on the assumption that checking groups up to order 1,000,000—often only the simple groups in that range—is enough to reveal counterexamples if they exist; if that search space is too small, some of the 40 'No Counter-examples' results could be false in larger or non-simple groups.

Editorial extensions

If this is right

  • If the pipeline works as reported, LLMs can usefully clear out the space around a newly invented mathematical object, generating simple plausible conjectures that human experts can then prove or refine.
  • The method transfers in principle to other computational mathematics domains—number theory, geometry, combinatorics—where a solver like SageMath or MAGMA can play the role GAP plays here.
  • The high rate of non-executable code (64.5% of unique outputs, and 81.9% for Gemini) means code generation, not conjecture generation, is the current bottleneck.
  • Because the models tend to reproduce known patterns and duplicates, the approach is best seen as fast exploration rather than a source of deep or fundamentally new mathematics.
  • Adding a formal theorem prover or proof engine to the loop could turn surviving conjectures into proved statements, making the system end-to-end.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A conjecture labeled 'No Counter-examples' is only as strong as the search space; extending the GAP search to non-simple non-solvable groups of order up to 1,000,000, or beyond that bound, could falsify some of the 40 survivors that the paper currently treats as plausible.
  • The cosine-similarity measure mostly captures syntactic wording, not mathematical content; two conjectures can be near-duplicates semantically while scoring as distinct, so the reported uniqueness fractions likely overstate diversity.
  • A natural testable extension would be to feed each model the other models' surviving conjectures and measure whether the pool's diversity grows; the paper's own suggestion of multi-model interaction could be evaluated quantitatively.
  • The 'interestingness' of a conjecture is left unmeasured; a concrete proxy—number of surviving conjectures that later become theorems, or that require a new proof technique—could make the pipeline's output more comparable across models.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes an LLM-based conjecture mining pipeline for the solubilizer Sol_G(x) in finite group theory. ChatGPT-4, Claude Sonnet, and Gemini 1.5 are prompted to generate conjectures and GAP code to test them; falsified conjectures are fed back into later prompts. From 757 raw outputs the authors identify 420 unique conjectures: 109 were falsified by counterexamples, 40 were labeled 'No Counter-examples', and 271 could not be executed. The paper concludes that LLMs can produce original, albeit simple, conjectures that are either plausible or falsifiable, while being limited in code execution.

Significance. The pipeline is described concretely and transparently: full prompts, a GAP code template, and a manual novelty check by an author of the original solubilizer papers are included. The use of an external computational algebra system (GAP) means the counterexample tests are not circular. The 109 falsified conjectures provide solid evidence for the 'falsifiable via counterexamples' half of the central claim. The contribution would be a useful small-scale demonstration of LLM-assisted conjecture screening if the 'No Counter-examples' category were properly scoped. As written, however, the plausibility claim is overreaching because the counterexample search is not over the universal domain stated in the conjectures, and at least one 'No Counter-examples' output is vacuous. The paper's value is therefore conditional on rescoping the claims and removing vacuous entries.

major comments (3)
  1. [Section 4.1, Listing 1, Appendix A.3.1] The 'No Counter-examples' label is based on checking only simple groups of order up to 10^6 in the default template (SimpleGroupsIterator(1,1000000)), and Appendix A.3.1 states that the runs checked 'all non-solvable (or in some cases just simple) groups of order up to 1,000,000'. The conjectures themselves quantify over all non-solvable groups, e.g., Conjecture 4.1. A property can hold for every simple group up to that bound yet fail on a non-simple non-solvable group such as a direct product S×C_p or a non-split extension, and the solubilizer's dependence on subgroups and radical subgroups means simple-group checks are not a sound reduction. The 40 'No Counter-examples' outputs therefore do not establish plausibility for the stated domain. The paper should either restrict all claims to 'no counterexamples in the tested simple groups' or extend the verification to all non-solvable groups of order at most 10^6.
  2. [Appendix A.4.3, Conjecture A.9] Conjecture A.9 has an unsatisfiable hypothesis. Setting y=1 gives ⟨x, xy⟩ = ⟨x,x⟩ = ⟨x⟩, which is cyclic and hence always solvable, directly contradicting the assumption '⟨x, xy⟩ is not solvable for any element y ∈ G'. The reported 'No Counter-examples' output is therefore vacuous, as the test code has no instance to check. This entry is counted among the 40 'No Counter-examples' results, suggesting that the total may include other vacuous statements. Each 'No Counter-examples' conjecture should be manually checked for satisfiability before being used as evidence of plausibility.
  3. [Appendix A.5.1] The proof of Conjecture 4.1 is logically invalid. From the fact that each maximal subgroup M of H = Sol_G(x) is contained in some maximal subgroup N of G, it does not follow that the intersection of all maximal subgroups of H is contained in the intersection of all maximal subgroups of G. A concrete counterexample to this inference is G = S_4 with H = C_4 embedded in the maximal subgroup D_8: Φ(C_4) is non-trivial while Φ(S_4) is trivial. The conjecture may still be true, but the appendix's proof does not establish it, and the paper's presentation of this as a successful model-generated proof is therefore overstated.
minor comments (4)
  1. [Section 3.1] The phrase 'solubilizer subset' is unclear; it should likely be 'solubilizer subfield' or 'solubilizer construction', since the solubilizer is a set-valued construct, not a subset in the sense used here.
  2. [Throughout] There are numerous typographical errors, e.g., 'dispuited', 'rememeber', 'similary', 'futher', and 'exampeled'. The manuscript would benefit from a careful proofreading pass.
  3. [Section 5.2] The sentence describing ChatGPT's conjectures contains a blank: 'the solubilizer couldn't be bigger than or that it couldn't be exactly equal to any of the following numbers'. The missing value or bound should be supplied.
  4. [Appendix A.6] The OpenAI o1 data are based on only 51 samples and are explicitly preliminary. The statement that 'o1 is the best one to use for this task in all aspects' is too strong for such a small sample and should be softened or clearly labeled as preliminary.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the LLM-generated conjectures are checked against an external computational oracle (GAP), and the only self-citation is a disclosed, non-load-bearing literature seed.

full rationale

The paper's central claim is an empirical pipeline result, not a mathematical derivation. Conjectures are generated by LLMs and then pruned by GAP code; the 'No Counter-examples' classification is an external computational test, not a quantity fitted from the same data and then re-reported as a prediction. The one reproduced literature conjecture (Theorem 5.1 / Conjecture 5.2) is explicitly attributed to the system prompt and excluded, so it does not force the originality claim. The cited solubilizer results, including the coauthor-involved [13], are used only as background context in the prompt; no load-bearing inference relies on an unverified self-citation. The main validity caveat is that the counterexample search covered only simple groups (or non-solvable groups up to 10^6) as disclosed in Appendix A.3.1, so 'no counterexamples' is narrower than the universal quantification of some conjectures; this is a correctness/scope limitation, not circularity, because the check is independent of the conjectures' formulation. No fitted parameter is renamed as a prediction and no definition is constructed in terms of the target result. Accordingly, no circular step can be exhibited with the required quote-and-reduction standard.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new mathematical objects. The solubilizer is from prior literature. All axioms are domain assumptions about the sufficiency and correctness of the empirical verification procedure.

assumptions (3)
  • domain assumption GAP's SimpleGroupsIterator over orders below 10^6 provides a sufficient test set for classifying a conjecture as having 'no counterexamples'.
    The paper labels 40 conjectures as having no counterexamples based on this limited search (Appendix A.3.1); if false, many such conjectures could be false in larger or non-simple groups.
  • domain assumption The manual comparison by one author against seven cited solubilizer papers is sufficient to establish that generated conjectures are original.
    Section 5.1 reports that 'one of the authors of the seven original solubilizer papers' verified all 420 unique conjectures for duplication; this is a subjective, single-reviewer check.
  • domain assumption The LLM-generated GAP code, when it runs, correctly computes solubilizers and group properties as intended.
    The whole counterexample-finding step assumes the GAP function and the model's code implement the mathematical definitions correctly; a bug would invalidate both 'failed' and 'no counterexamples' labels.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Mining Math Conjectures from LLMs: A Pruning Approach." pith.science (2026). https://pith.science/paper/JBGUH7XI

@misc{pith2026241216177,
  author       = {Pith},
  title        = {Pith review of: Mining Math Conjectures from LLMs: A Pruning Approach},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JBGUH7XI}},
  note         = {Machine review of arXiv:2412.16177}
}
read the original abstract

We present a novel approach to generating mathematical conjectures using Large Language Models (LLMs). Focusing on the solubilizer, a relatively recent construct in group theory, we demonstrate how LLMs such as ChatGPT, Gemini, and Claude can be leveraged to generate conjectures. These conjectures are pruned by allowing the LLMs to generate counterexamples. Our results indicate that LLMs are capable of producing original conjectures that, while not groundbreaking, are either plausible or falsifiable via counterexamples, though they exhibit limitations in code execution.

Figures

Figures reproduced from arXiv: 2412.16177 by the authors.

Figure 1
Figure 1. Method 4 Results 4.1 Performance Overview The experiment provided three types of outcomes (Summarized in [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. GPT-4 Cosine Self Similarity 15 [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗
Figure 3
Figure 3. Claude Cosine Self Similarity 16 [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Gemini Cosine Self Similarity 17 [PITH_FULL_IMAGE:figures/full_fig_p017_4.png]
Figure 5
Figure 5. Figure 5: GPT vs. Claude Cosine Similarity 18 [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]
Figure 6
Figure 6. Figure 6: GPT vs. Gemini Cosine Similarity 19 [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 7
Figure 7. Figure 7: Claude vs. Gemini Cosine Similarity 20 [PITH_FULL_IMAGE:figures/full_fig_p020_7.png]
Figure 8
Figure 8. Figure 8: Gemini vs. Literature Cosine Similarity 21 [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. Figure 9: Claude vs. Literature Cosine Similarity 22 [PITH_FULL_IMAGE:figures/full_fig_p022_9.png]
Figure 10
Figure 10. Figure 10: GPT-4 vs. Literature Cosine Similarity 23 [PITH_FULL_IMAGE:figures/full_fig_p023_10.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 31 canonical work pages

  1. [1]

    GPT-4 Technical Report,

    OpenAI, “GPT-4 Technical Report,” 2023

    2023

  2. [2]

    Claude AI

    Anthropic, “Claude AI.” Available at: https://www.anthropic.com, 2023

    work page 2023

  3. [3]

    Gemini: A family of highly capable multimodal models,

    G. Team, R. Anil, S. Borgeaud, and et al., “Gemini: A family of highly capable multimodal models,” 2024

    work page 2024

  4. [4]

    Would ChatGPT3 Get a Wharton MBA? A Prediction Based on Its Performance in the Operations Management Course,

    C. Terwiesch, “Would ChatGPT3 Get a Wharton MBA? A Prediction Based on Its Performance in the Operations Management Course,” Mack Institute for Innovation Management at the Wharton School, University of Pennsylvania, 2023

    work page 2023

  5. [5]

    Mathematical discoveries from program search with large language models,

    B. Romera-Paredes, M. Barekatain, A. Novikov, et al., “Mathematical discoveries from program search with large language models,” Nature, vol. 625, pp. 468–475, 2024

    work page 2024

  6. [6]

    Exploring mathematical conjecturing with large language models,

    M. Johansson and N. Smallbone, “Exploring mathematical conjecturing with large language models,” in NeSy, pp. 62–77, 2023

    work page 2023

  7. [7]

    Advancing mathematics by guiding human intuition with AI,

    A. Davies, P. Veliˇckovi´c, L. Buesing, et al., “Advancing mathematics by guiding human intuition with AI,” Nature, vol. 600, pp. 70–74, 2021

    work page 2021

  8. [8]

    Autoformalization with large language models,

    Y . Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy, “Autoformalization with large language models,” ArXiv, vol. abs/2205.12615, 2022

    arXiv 2022

Show all 33 references
  1. [9]

    Can LLMs generate novel research ideas? A large-scale human study with 100+ NLP researchers,

    C. Si, D. Yang, and T. Hashimoto, “Can LLMs generate novel research ideas? A large-scale human study with 100+ NLP researchers,” 2024

    2024

  2. [10]

    More on the non-solvable graphs and solvabilizers,

    B. Akbari, “More on the non-solvable graphs and solvabilizers,” 2018

    2018

  3. [11]

    The solubility graph associated with a finite group,

    B. Akbari, M. L. Lewis, J. Mirzajani, and A. R. Moghaddamfar, “The solubility graph associated with a finite group,” 2020

    2020

  4. [12]

    On the solubilizer of an element in a finite group,

    B. Akbari, C. Delizia, and C. Monetta, “On the solubilizer of an element in a finite group,” 2022

    2022

  5. [13]

    Characterization of solubilizers of elements in minimal simple groups,

    B. Akbari, J. Chuharski, V . Sharan, and Z. Slonim, “Characterization of solubilizers of elements in minimal simple groups,” 2023

    2023

  6. [14]

    Non-solvable graph of a finite group and solvabilizers,

    D. Hai-Reuven, “Non-solvable graph of a finite group and solvabilizers,” 2013

    2013

  7. [15]

    Solubilizers in profinite groups,

    A. Lucchini, “Solubilizers in profinite groups,” 2023

    2023

  8. [16]

    The impact of the solubilizer of an element on the structure of a finite group,

    H. Mousavi, M. Poozesh, and Y . Zamani, “The impact of the solubilizer of an element on the structure of a finite group,” 2023

    2023

  9. [17]

    Is Temperature the Creativity Parameter of Large Language Models?,

    M. Peeperkorn, T. Kouwenhoven, D. Brown, and A. Jordanous, “Is Temperature the Creativity Parameter of Large Language Models?,” 2024

    2024

  10. [18]

    SageMath, the Sage Mathematics Software System (Version 10.0),

    W. A. Stein et al., “SageMath, the Sage Mathematics Software System (Version 10.0),” The Sage Developers, 2023. [Online]. Available: https://www.sagemath.org

    2023

  11. [19]

    Integrating multiple sources to answer questions in Algebraic Topology,

    J. Heras, V . Pascual, A. Romero, and J. Rubio, “Integrating multiple sources to answer questions in Algebraic Topology,” arXiv preprint arXiv:1005.0749, 2010. [Online]. Available: https: //arxiv.org/abs/1005.0749

    2010 arXiv

  12. [20]

    GSM- Symbolic: Understanding the limitations of mathematical reasoning in large language models,

    I. Mirzadeh, K. Alizadeh, H. Shahrokhi, O. Tuzel, S. Bengio, and M. Farajtabar, “GSM- Symbolic: Understanding the limitations of mathematical reasoning in large language models,” 2024

    2024

  13. [21]

    Solving Olympiad Geometry Without Human Demonstra- tions,

    T. H. Trinh, Y . Wu, Q. V . Le, et al., “Solving Olympiad Geometry Without Human Demonstra- tions,” Nature, vol. 625, pp. 476–482, 2024

    2024

  14. [22]

    AI solves IMO problems at silver medal level,

    DeepMind, “AI solves IMO problems at silver medal level,” 2023. 6

    2023

  15. [23]

    Nonsolvable finite groups all of whose local subgroups are solvable,

    J. H. Thompson, “Nonsolvable finite groups all of whose local subgroups are solvable,”Bull. Am. Math. Soc., vol. 48, no. 2, pp. 511–592, 1973

    1973

  16. [24]

    Thompson-like characterization of the solvable radical,

    R. Guralnick, B. Kunyavski˘ı, E. Plotkin, and A. Shalev, “Thompson-like characterization of the solvable radical,” J. Algebra, vol. 300, no. 1, pp. 363–375, 2006

    2006

  17. [25]

    Introducing OpenAI O1-preview

    OpenAI, “Introducing OpenAI O1-preview.” Available at: https://openai.com/index/ introducing-openai-o1-preview , 2024. Accessed: 2024-09-20. A Appendix / Supplemental Material A.1 Acknowledgements We would like the thank Tomaso Poggio and Brian Cheung for helpful discussions a...

    2024

  18. [26]

    This is the smallest subgroup of G that contains both x and y

    ⟨x, y⟩ denotes the subgroup of G generated by the elements x and y. This is the smallest subgroup of G that contains both x and y

  19. [27]

    The condition that ⟨x, y⟩ is solvable means that there exists a sequence of subgroups, starting with the trivial group and ending with ⟨x, y⟩, such that each subgroup in the sequence is a normal subgroup of the next, and the quotient of successive subgroups is abelian. 7

  20. [28]

    This is an interesting definition, and it essentially captures the elements in G that, when paired with x, produce a solvable subgroup

    The solubilizer SolG(x) is then the set of all elements y in G for which this condition holds. This is an interesting definition, and it essentially captures the elements in G that, when paired with x, produce a solvable subgroup. The concept seems to be related to understandi...

  21. [29]

    Theorem: For any x ∈ G, x ∈ SolG(x)

    Non-Empty Solubilizer: For any element x in G, x belongs to SolG(x) because the subgroup ⟨x⟩ (generated solely by x) is cyclic and hence solvable. Theorem: For any x ∈ G, x ∈ SolG(x)

  22. [30]

    This is because if ⟨x, y⟩ is solvable, then ⟨x, y−1⟩ is also solvable

    Subgroup Containment: If y belongs to SolG(x), then y−1 (the inverse of y) also belongs to SolG(x). This is because if ⟨x, y⟩ is solvable, then ⟨x, y−1⟩ is also solvable. Theorem: For any y ∈ SolG(x), y−1 ∈ SolG(x)

  23. [31]

    Theorem (Conditional): For y1, y2 ∈ SolG(x), if y1y2 ∈ ⟨x, y1⟩ or y1y2 ∈ ⟨x, y2⟩, then y1y2 ∈ SolG(x)

    Closure under Solvability: If y1, y2 ∈ SolG(x) and their product y1y2 belongs to ⟨x, y1⟩ or ⟨x, y2⟩, then y1y2 should also belong to SolG(x). Theorem (Conditional): For y1, y2 ∈ SolG(x), if y1y2 ∈ ⟨x, y1⟩ or y1y2 ∈ ⟨x, y2⟩, then y1y2 ∈ SolG(x)

  24. [32]

    Theorem: If G is solvable, then for all x ∈ G, SolG(x) = G

    Entire Group Solvability: If G itself is solvable, then for any x ∈ G, SolG(x) = G. Theorem: If G is solvable, then for all x ∈ G, SolG(x) = G

  25. [33]

    No Counter - examples !

    Size of the Solubilizer: The size of SolG(x) provides information about the complexity of the group’s structure in relation to solvability. Conjecture: For certain classes of groups (e.g., simple groups), the size of SolG(x) relative to the order of G may have particular bound...

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.