Mining Math Conjectures from LLMs: A Pruning Approach

Authors: jake  chuharski
elias  rojas collins
mark  meringolo
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-24 22:33:42

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.

Main paper: 
 introduction: 
 Artificial intelligence, specifically deep learning, has created much discussion around the possibility to augment human creativity with computational capability. Among the leading technologies pushing this discussion are large language models (LLM's) such as OpenAI's ChatGPT, Anthropic's Claude, and Google's Gemini (1; 2; 3). While LLMs have been widely recognized for their competence in text generation, their interactions within abstract academic fields such as mathematics, specifically with conjecture creation, remain under-explored. Initial work has evaluated LLMs' ability to pass exams like the SAT and MBA qualifying exams (4; 1). More recently, efforts have focused on bench-marking their capacity to generate mathematical proofs (5) . However, there has been little work on bench-marking the ability of language models to act as a creative agent towards coming up with new conjectures.In this study, we use the Claude Sonnet, Gemini 1.5, and GPT-4 APIs to both generate conjectures and write GAP computer algebra code to check them for plausibility. GAP (Groups, Algorithms, and Programming) is a computer algebra system designed for computational group theory and related areas in abstract algebra. However, GAP is not a proof assistant so does not give the user proofs for theorems, but it can be used to check conjectures for immediate counterexamples. We work specifically on the solubilizer subset which is a relatively new/unexplored construction in group theory that contains much potential for novel conjectures (see Appendix A.1). GAP computer algebra can check the conjecture for chosen groups and allows for language models to "guess and check".The system provides a method to mine for conjectures using language models and a pruning step to remove conjectures that are false for obvious (or sometimes non-obvious) reasons. This approach offers a systematic method for generating and validating conjectures, combining model output with automated computational verification without requiring a strong formal theorem prover.If the code compiles and runs and the outcome is recorded. If the code does not compile the LLM is prompted again to fix the code, provided with the output of the failing program. It is given the chance to do two revisions (in practice allowing for further revision almost never results in working code). 3. If the result is that the conjecture is false, the theorem and it's result is added to the prompt, and the process is repeated with the false conjecture added to the set of ideas that are known to fail.This process was run with three models: ChatGPT 4 (gpt-4o-2024-05-13), Claude Sonnet (claude-3-5-sonnet-20240620), and Gemini 1.5 (gemini-1.5-flash). LLM's have a "Temperature" parameter which varies the level of randomness in the outputs to a given prompt. This is sometimes taken as a proxy for "Creativity", although this description is dispuited (17) . The temperature for the Claude model was set to 1 for conjecture generation and .1 for code generation. The GPT-4 conjecture was set to 1.08 for conjecture generation and was left at default for code generation. The Gemini 1.5 conjecture generation was set to 1.5 (top_k: 5, top_p:.99) and default for code generation. The values were generated by trial and error where the authors observed qualitatively the most consistent conjecture variation without extreme hallucinations2 . 
subgroup containment:: 
 If y belongs to Sol G (x), then y -1 (the inverse of y) also belongs to Sol G (x). This is because if ⟨x, y⟩ is solvable, then ⟨x, y -1 ⟩ is also solvable. Theorem: For any y ∈ Sol G (x), y -1 ∈ Sol G (x).3. Closure under Solvability: If y 1 , y 2 ∈ Sol G (x) and their product y 1 y 2 belongs to ⟨x, y 1 ⟩ or ⟨x, y 2 ⟩, then y 1 y 2 should also belong to Sol G (x). Theorem (Conditional): For y 1 , y 2 ∈ Sol G (x), if y 1 y 2 ∈ ⟨x, y 1 ⟩ or y 1 y 2 ∈ ⟨x, y 2 ⟩, then y 1 y 2 ∈ Sol G (x). 
area of focus: 
 The mathematical area of focus is called the solubilizer and is defined as follows: Definition 3.1. Let G be a finite group. For any element x ∈ G, the solubilizer of x in G is defined as:Sol G (x) := {y ∈ G | ⟨x, y⟩ is soluble}.More introductory and historical information on the solubilizer can be found in the Appendix A.1.  
performance overview: 
 The experiment provided three types of outcomes (Summarized in Table 3 ):• Successful generation of counterexample-finding code in 25.95% of cases (109 out of 420 unique outputs). • Generation of conjectures without counterexamples in 9.52% of cases (40 out of 420 unique outputs). • Generation of non-executable code in 64.52% of cases (271 out of 420 unique outputs). Where PSL(3, 2) is the projective special linear group of 3x3 matrices over the finite field F 2 . Lastly, we have an example where code could not be executed from GPT-4: Conjecture 4.4. Let G be a finite non-solvable group and x ∈ G. Then for every abelian subgroup A of G, we have Sol G (x) ∩ A ̸ = {1}.To quantitatively measure diversity, we calculated the cosine self-similarity, and similarity between conjecture sets/literature. The similarity results are summarized in Table 2 . Where we see a maintained level of similarity throughout the experiments and between models. See Appendix A.7 for heatmaps.Scaling the system further by increasing the number of trials or generating more variations in the prompt failed to yield significantly more diverse conjectures. However the quality did not decrease either. This finding suggests that a different approach, such as multi-modal model interaction or combining LLMs with automated theorem provers, could help diversity. If G itself is solvable, then for any x ∈ G, Sol G (x) = G. Theorem: If G is solvable, then for all x ∈ G, Sol G (x) = G. 
observations: 
 Among the 757 outputs generated by the LLMs, 420 unique conjectures were identified. The high number of duplicates shows a considerable redundancy in the results, as approximately 55.48% of the conjectures were deemed to be unique. While not unexpected, the duplicates suggest that LLMs likely rely on similar patterns when prompted similarly across trials as described in (6) . However, this did not significantly hinder overall performance other than increase the number of total iterations needed to yield a desirable number of conjectures.Not all of the conjectures generated by the models were entirely original and was verified by one of the authors of the seven original solubilizer papers for all 420 unique conjectures. For example, Theorem 5.1. Let G be an insoluble group and x an element of G. Then the cardinality of cannot be equal to p 2 for any prime p.shows up in (12) and GPT-4 conjectured: Conjecture 5.2. Let G be an insoluble group and x ∈ G. Then the cardinality of Sol G (x) cannot be equal to p 2 for any prime p.That being said, this result was contained in the system prompt and can be ignored. In all other cases the models output conjectures that were distinct from anything found in literature or their system prompt.In 109 cases (25.95%), the generated code successfully identified counterexamples, which is critical for falsifying conjectures. Secondly, of the 420 unique outputs, only 40 (9.52%) produced conjectures with no counterexamples. ChatGPT significantly outperformed both Claude and Gemini in this area, generating 26.60% valid conjectures compared to Gemini's 4.64% and Claude's 4.49%. This shows that ChatGPT was more effective at producing conjectures that are plausible at first glance. However, a large portion of the GPT-4 conjectures were looking at the size of the solubilizer rather than about interactions with other groups, group structure, or subgroup properties. Therefore, one could argue that they were easier to write code for, or at least more likely to succeed based on similarity. Further still, results classified as having "no counterexamples" by GPT-4 seemed to be qualitatively more obvious than those by Claude or Gemini (see Conjecture A.5 vs. Conjecture A.4 vs. Conjecture A.9). Lastly, the fact that the models are able to generate novel, original conjectures at all provides promise for these models to be used as useful tools when developing the theory of a new construction.A limitation observed in both models was the generation of non-executable code, which occurred in 271 instances (64.52% of unique outputs). Gemini and Claude struggled more with code execution, having 81.86% and 49.44% instances of non-executable code respectively, compared to ChatGPT's 37.76%. This potentially points to differences in how the models handle code syntax in GAP, however the models were prompted to have a near identical code format (see Appendix A.2). This corroborates the idea that some conjectures set by Claude/Gemini are more difficult to write code for, and therefore more likely to fail in this system. Interestingly, there are some examples that Claude/Gemini gave that would be much harder to check in GAP with a constrained time limit where Claude/Gemini could not write executable code (see Appendix A.4.6). Lastly, we note that the models had different approaches to generating code to test conjectures, with Claude and Gemini being more similar. We found that ChatGPT liked to preemptively restrict the groups it would consider. For example, ChatGPT conjectured that the solubilizer couldn't be bigger than or that it couldn't be exactly equal to any of the following numbers (for all non-solvable groups) in seperate conjectures: [2, 3, 6, 8, 9, 10, 11, 12, 14, 15, 16, 18, 20, 24, 25, 27, 32, 49, 50, 126] .While this study focuses on group theory and solubilizers, a relatively unexplored area, the approach could be generalized to other domains. We acknowledge limitations of using GAP, an algebra software. However, future work could easily extend this methodology to fields like number theory, geometry, representation theory, or combinatorics by integrating tools like SageMath, MAGMA, or other computational solvers.We propose the investigation of conjecture generation in fields where existing conjectures are sparse or absent. For example, LLMs could be applied to generate conjectures in newer or less explored areas such as tropical geometry or higher homotopy theory, where automated tools exist but have yet to be fully integrated with LLMs. Furthermore, the study above was limited to using a single LLM. If one model is better at writing code and the other is better at conjectures, using a combination structure could yield better results. We remark that a quantitative metric for 'interestingness' of a math conjecture or problem seems to be elusive, nontrivial, yet useful (see Appendix A.6).The size of Sol G (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 Sol G (x) relative to the order of G may have particular bounds or properties.All five of these ideas are true. The first four are easily proved to be correct mathematical statements and the fifth is just a general statement that presents the (correct) expectation that the solubilizer may be informative to studying the structure of the group. 
conclusion: 
 The study opens up several promising avenues for the use of LLMs in research. Our work, while small, shows the potentially impactful way that LLM's augmented with other computational capacity can solve more complex problem. For example, further work integrating conjecture generation with proof validation systems could streamline the process of discovery.That being said, LLM-based conjecture generation is still very limited to existing knowledge. Rather than producing fundamentally new ideas, LLMs are likely to lean on known results, limiting their ability to drive groundbreaking discoveries (18) . Indeed, when thinking of language models as statistical traversers of some sort of higher dimensional surface built from training data, it is easy to imagine that the models are not able to stray too far from what they are fed to generate the surface. Specifically, conjectures and theorems involving well-understood subgroups on which the solubilizer is inspired (think centralizer and normalizer) can serve as an incredibly large well from which an LLM can sample a new direction about the solubilizer. This may all be permissible to a practitioner if one is only interested in clearing out the brush around a new construct such as the solubilizer; but as of writing, it should not be expected that these models will conjecture something profound.We demonstrate that combining LLMs with computational resources like GAP can successfully generate and test original, albeit simple math conjectures. Indeed, performance suggests that LLMs like ChatGPT, Claude, and Gemini have potential, but only on conjectures that are similar to existing ideas or are otherwise simple. Furthermore, the models face significant challenges in generating executable code and avoiding duplicate conjectures. Indeed, ChatGPT-4 demonstrated stronger performance in generating conjectures that could not be immediately falsified, Claude was slightly more effective at identifying counterexamples, and Gemini had the least redundancy likely due to the longer context window. The high percentage of non-executable code reinforces the need for robust error-checking and handling within the models. GAP is limited in the variety of error codes that are produced when code fails, so other more verbose computational algebra solvers could help with error correction. Lastly, further analysis of failed code generation to find patterns of failure could lead to better prompting for avoiding common bugs. Further work would likely include adding a formal automated theorem prover or another form of neuro-symbolic proof engine, giving an end-to-end system that can generate new conjectures and prove them in a single pass (19; 20) . The authors are also interested to see other new approaches for accurate conjecture generation in various abstract fields, or more generally, improvements to conjecture generation by non-LLM based models. 
 
 Appendix: A.1 SolubilizerThe solubilizer is a construct that can be attributed to Doron Hai-Reuven in ( 14) from 2013. Much of the work in the area can be atributed to Banafsheh Akbari et al. in (10; 11; 12; 13) . The construct itself should be intelligible for anyone who has taken an introductory university algebra course, although can be potentially unpredictable to work with. It is therefore also simple for the models to understand, but non-trivial to produce conjectures. All of the models claim to have not heard of the construction before, meaning that the training data either excluded this information or did not have enough for it to be in the knowledge base. In either case, the models seem to be able to understand the definition once it is given, and provide often accurate assumptions about how the set behaves. For example, when testing these ideas on GPT-4, the model responded with the following:Input: Give me the definition of the solubilizer in group theoryOutput: "In group theory, there isn't a concept specifically called 'solubilizer.' However, I suspect you might be referring to the 'solubility' of a group or the concept of a 'solvable group.' A group G is said to be solvable if there exists a sequence of subgroups{e} = G 0 ◁ G 1 ◁ G 2 ◁ • • • ◁ G n = Gsuch that each G i is a normal subgroup of G i+1 and the quotient group G i+1 /G i is abelian. Solvable groups generalize the notion of abelian groups. Solvability is an important property in group theory and plays a key role in Galois theory, which connects group theory with field theory. If you had a different concept in mind or need more information about solvable groups or another topic, please clarify, and I'll be happy to assist further!"We also further note that the model presents an almost identical response to "solvabilizer" instead of "solubilizer" which is another name that the set can be found under in the literature. We then present the definition to the model so that it can begin to formulate an understanding of the area.Input: I will define the solubilizer as follows: Let G be a finite group. For an element x in G, we define the solubilizer of x in G as the set: SolG(x) := {y ∈ G|⟨x, y⟩ is soluble} Output: "Ah, I see. Given your definition, the solubilizer Sol G (x) of an element x in G is the set of all elements y in G such that the subgroup generated by x and y, denoted ⟨x, y⟩, is a solvable group.To further elaborate on this:1. ⟨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. 2. 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. 3. The solubilizer Sol G (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 understanding the structure and solvability properties of subgroups within G. Do you have specific questions about this definition or its properties?"This output shows three correct assertions about the subset, so we test to see if the model can expand further on it's understanding without more input. The model is then asked to provide some conjectures based on the newly learned definition. The idea is to gauge the model's understanding of a single definition and to see what material the model relates to the new definition to conjecture something that it considers to be new material.Input: Based on this definition, can you conjecture any theorems that might apply to this set? Output: "Certainly! Given the definition of the solubilizer Sol G (x) in a finite group G, we can propose some conjectures or theorems. Here are a few ideas:1. Non-Empty Solubilizer: For any element x in G, x belongs to Sol G (x) because the subgroup ⟨x⟩ (generated solely by x) is cyclic and hence solvable. Theorem: For any x ∈ G, x ∈ Sol G (x).Let G be a finite group, and for any element x ∈ G, the solubilizer of x in G is defined as:Sol G (x) := {y ∈ G | ⟨x, y⟩ is soluble}.In general, Sol G (x) is not necessarily a subgroup of G. However, there are specific conditions under which this set does form a subgroup. It has been proven in (14) that Sol G (x) is a subgroup of G for any element x ∈ G if and only if G is a soluble group.A well-known result, attributed to Thompson (21) , states that a finite group G is soluble if and only if, for every x, y ∈ G, the subgroup ⟨x, y⟩ is soluble. Thus, a finite group G is soluble if and only if for any elementx ∈ G Sol G (x) = G.An important related concept is the soluble radical R(G), the largest soluble normal subgroup of G. Guralnick et al. (22) demonstrated that for an element x ∈ G, x ∈ R(G) if and only if ⟨x, y⟩ is soluble for all y ∈ G. Consequently,x ∈ R(G) if and only if Sol G (x) = G.A common question is how the structure of a single solubilizer influences the structure of the entire group. For instance, it was shown in ( 14) that if G contains an element x such that all elements of Sol G (x) commute pairwise, then G must be abelian. Another example, (11) generalizes this by proving that if there exists x ∈ G such that for everyu 1 , u 2 , u 3 ∈ Sol G (x), the commutator [u 1 , u 2 , u 3 ] = 1, then γ 3 (G) = 1,implying that the group is nilpotent. Here, γ 3 (G) is the third term in the lower central series of G. These are ideas that are more often explored by Claude and Gemini, although are harder to verify.The arithmetic properties of solubilizers also play a crucial role in determining group structure. For example, if G contains an element x whose solubilizer has order p or p 2 (where p is a prime), then G is a p-group, as discussed in (12) . These ideas seem to be of heavy focus for ChatGPT.Thompson's theorem (21) demonstrated that a finite group G is soluble if and only if every twogenerated subgroup of G is soluble. This motivates the definition of the solubilizer and highlights its significance. Moreover, the solubilizer operates similarly to the centralizer in a group, with the soluble radical R(G) functioning in a way comparable to the center of a group. Analogous to the centralizer C G (x) = {y ∈ G | ⟨x, y⟩ is abelian}, the solubilizer describes solvability rather than commutativity. However, unlike the centralizer, the solubilizer is not always a subgroup which was initially tough for the models to rememeber, leading to this fact requiring repetition in the prompting.Both the prompt for generating conjectures and the prompt for generating code were prefaced with:""" You are a mathematician and efficient computer scientist . You are interested in abstract algebra , but are generally very knowledgeable and interested in the intersections between different areas of math .You have began working on the ' solubilizer ' subset of a nonsolvable group . You are very good at writing GAP code . The user will ask for either a conjecture , or GAP code to check a conjecture .When a user asks for GAP computer algebra code you will provide nothing in your response except code to complete their task . When writing code make sure that the answer to your question is PRINTED to the terminal .A maximum of two things should be printed by your code . If the conjecture fails , the code should break and just print for which group the conjecture failed . If the code does not generate any counter -examples , the code should return " No Counter -examples !".Additionally , make sure you only test conjectures on Non -Solvable groups ! For example , when checking a conjecture , you might want to check it on all non -solvable groups of order less than one million by using : SimpleGroupsIterator (1 , 10^6) . This means ONLY give GAP computer algebra code unless the user asks for a conjecture . When the user asks for a conjecture you should return nothing but the conjecture .""" The code generation system prompt for both models included code snippets for how to accurately and consistently generate the solubilizer and had the format for how the conjectures should be checked and output. end ; " When you test a conjecture . Make sure to have the end of your code be in this format " :Here we briefly summarize data taken from OpenAI o1 (23) . Due to initial limiting factors and the short timeline, the authors have not finished gathering sufficient data to be included into the main body. We recieved 51 conjectures with the following data: Perhaps unsurprisingly, the new model was able to execute code properly roughly 98% of the time. Furthermore, the model only once needed to take a debug step. The authors believe that the conjectures are not any significantly more interesting than the other ones given by Gemini and Claude, although this model does give more interesting conjectures than GPT-4 in terms of the willingness to give conjectures about relation of the solubilizer to other subgroups, conjugacy classes, etc. We note that this model was more willing to stray from the system prompt in the GAP code wherein it generated code that checked non-solvable groups that were not simple. Lastly, observe that all of the conjectures are unique, which leaves this model so far being (albeit with a lower than desireable number of samples to make a strong claim) the best one to use for this task in all aspects. The authors intend to explore this further in the coming weeks.The following are four randomly chosen examples and their output. Conjecture A. The system failed to write code for a single conjecture: Conjecture A.26. In any finite group G, the solubilizer Sol G (x) is invariant under all automorphisms of G that fix x.In mathematics, evaluating the "interestingness" of a conjecture or problem is inherently subjective and resists quantification. However, if one seeks a quantitative approach, there are several aspects to be considered: the conjecture's depth, its generality or specificity, its implications for other fields, simplicity of solution, and whether it leads to significant advancements or novel methods. Indeed, some of these are impossible to predict, and are not always necessary for a conjecture to be labeled interesting. Some conjectures, like the Riemann Hypothesis, have clear applications to a wide range of fields, yet others garner interest without obvious practical use. Consider the Collatz Conjecture: despite its straightforward formulation, the conjecture resists resolution and has few known applications, yet it draws wide attention due to its seemingly simple, though elusive nature. Furthermore, a conjecture's "interestingness" often depends on historical context, cultural influence within mathematical communities, and its perceived difficulty or elegance.Another difficulty in quantifying interestingness is the risk of conflating technical complexity with profundity. A conjecture could be formally intricate yet lack broader appeal or connection to other domains. Additionally, highly specialized conjectures may be overlooked by non-specialists despite their beauty or importance for those knowledgebale in the field. Further, the evolving nature of mathematical interest itself becomes an issue; conjectures once regarded as obscure can gain recognition as foundational connections become clearer.Nevertheless, certain conjectures seem almost universally intriguing. The Poincaré Conjecture and Fermat's Last Theorem captivated broad attention due to their simplicity, profound implications, and historical legacy. If just pieces of these ideas could somehow be built into a standardized metric, many studies will surely benefit.We include figures that show the similarity heatmaps between conjectures below. It is visually apparent from these maps that Claude in general had the most syntactic similarity. Indeed, with conjectures exampled as the following A.27A.28, the entire structure of the first conjecture is held within the second but they are not the same idea. Conjecture A.27. "Let G be a finite non-solvable group. Then for any element x in G, if Sol G (x) is a proper subgroup of G, there exists a prime p dividing |G| such that Sol G (x) intersects at least two distinct Sylow p-subgroups of G non-trivially." Conjecture A.28. Let G be a finite non-solvable group. Then for any element x in G, if Sol G (x) is a proper subgroup of G, there exists a prime p dividing |G| such that Sol G (x) intersects at least two distinct Sylow p-subgroups of G non-trivially, but does not contain any full Sylow p-subgroup of G.GPT-4 clearly has the most syntactic differences in the conjectures. While many of the conjectures reference the same idea, the way that they are stated is highly variable. Claude and Gemini both have a more methodical approach which show up as lighter colored squares. One can see that Gemini also had a period of runtime where the conjectures were mostly structured similarly with different modifiers at the end of the conjecture. The authors are unsure why these structural 'loops' seem to occur periodically throughout the repeated process, but they are interesting to note regardless. In these patches there didn't seem to be a significant difference in the quality of conjecture.With regards to the similary with the literature, non-surprisingly GPT-4 had the highest similarity due to the reproduction of a conjecture from literature as noted above. Otherwise, the distinction in the models between themselves was roughly comparable with that in literature. We note that Claude had the lowest maximum similarity, that all of the models had a minimum similarity of zero, and that on average, the models were slightly more disjoint from literature than they were from each other. For example, if the temperature is set too high in GPT-4, the model will return output in multiple languages 


Decision: Reviewers find the approach of generating conjectures using LLMs and GAP interesting and novel. The paper could improve by having more comprehensive analysis and discussion of the results, but seems to be a worthwhile contribution to the workshop.

Reviews: review: title: title: Rigorous Experimental Design
main_review: main_review: This study explores the integration of large language models (LLMs) with computational tools like GAP to successfully generate and test original mathematical conjectures. The results demonstrate the potential of combining these technologies to make significant strides in mathematical discovery. The models show promise, although there are minor challenges in generating executable code and avoiding duplicate conjectures.

The strengths of this paper lie in its rigorous experimental design and the substantial amount of testing conducted, which thoroughly validates the approach. However, one notable weakness is the lack of clarity on the significance of creating original mathematical conjectures and why this area is worth exploring. The paper’s contribution to the field also feels somewhat ambiguous and would benefit from a more detailed explanation of its impact and relevance
title: title: Interesting approach to generate conjectures in algebra
main_review: main_review: Summary: 
The paper introduces a novel approach for generating mathematical conjectures by combining LLMs with the GAP computer algebra system. The paper explores how LLMs can suggest conjectures, and how GAP is used to find counter-examples to these conjectures.

Strengths:
- An interesting approach, combining LLMs with GAP code.
- Clear writing style.

Opportunities for improvements:
- I was hoping the authors could discuss both the diversity of the generated conjectures, and the limitations of the approach in a more quantitative way: How diverse are the final conjectures? Does scaling the approach allow generating more and more conjectures or does the process reach a point of diminishing returns?
- The scope of this paper appears to be limited to conjectures in the field of algebra, as the approach uses GAP, which can only be used in algebra. A discussion on a possible generalization of the approach to other fields could be interesting. 

Final remark: 
The approach introduced in this paper is interesting, and I believe the workshop can benefit from the paper discussion. However, given the limitations of the approach (diversity, scaling, limited to algebra), I opt to give a rating of 6.
title: title: Evaluating LLMs for Mathematical Conjecture Generation
main_review: main_review: This paper presents an interesting approach to leveraging large language models (LLMs) for generating and evaluating mathematical conjectures, focusing on the domain of group theory and the concept of solubilizers. The authors use ChatGPT, Gemini, and Claude to generate conjectures about solubilizers and then employ the GAP computer algebra system to test these conjectures on non-solvable groups.

Pros:
1. Novel application: The paper explores an innovative use of LLMs in mathematics, specifically for conjecture generation, which is an under-explored area.
2. Methodology: The authors present a clear methodology for generating and pruning conjectures using LLMs and computational tools.
3. Comparative analysis: The study compares the performance of multiple LLMs (ChatGPT, Gemini, Claude), providing insights into their relative strengths and weaknesses.
4. Domain selection: Focusing on solubilizers, a relatively new concept in group theory, helps ensure the originality of the generated conjectures.
5. Practical implications: The approach could potentially assist mathematicians in exploring new areas and generating novel hypotheses.

Cons:
1. Limited scope: The study focuses solely on group theory and solubilizers, which may limit the generalizability of the findings to other areas of mathematics.
2. Sample size: The number of generated conjectures (430 unique outputs) is relatively small, which may affect the statistical significance of the comparisons between models.
3. Evaluation criteria: The paper lacks a clear framework for evaluating the quality and novelty of the generated conjectures beyond their immediate falsifiability.
4. Human expert validation: There is no mention of human mathematicians evaluating the generated conjectures for their potential significance or novelty.
5. Limited discussion of practical applications and broader impact: The authors do not sufficiently explore the potential real-world applications and broader implications of their work. While they mention that this approach could assist mathematicians, they do not delve into how it might transform mathematical research practices, accelerate discoveries in other fields that rely on mathematical foundations, or impact mathematics education. The paper would benefit from a more thorough discussion of how this AI-driven approach to conjecture generation could influence the broader scientific community, potentially leading to breakthroughs in related fields such as physics, computer science, or cryptography. Additionally, the authors could have addressed how this technology might be integrated into mathematical software tools or research workflows, and its potential to democratize mathematical discovery by making it more accessible to researchers with varying levels of expertise.

General Comments:
- The paper demonstrates that LLMs can indeed generate plausible mathematical conjectures and, in some cases, produce original ideas that warrant further investigation. The methodology of using LLMs for generation and computational tools for validation is sound and could be extended to other areas of mathematics.
- The authors provide a thorough analysis of the performance of different LLMs, highlighting their strengths and limitations. For instance, ChatGPT showed better performance in generating conjectures that could not be immediately falsified, while Claude was more effective at identifying counterexamples.
- However, the paper would benefit from a more rigorous evaluation of the quality and potential impact of the generated conjectures. Involving human experts to assess the most promising conjectures could provide valuable insights into the practical utility of this approach.
- The discussion of the limitations of LLMs in executing code and the high percentage of non-executable code (63.02% of unique outputs) is particularly insightful. This highlights an area for improvement in LLM training and prompts further research into enhancing their code generation capabilities.
- The authors' suggestion for future work, including the integration of automated theorem provers or neuro-symbolic proof engines, is promising and could lead to more robust end-to-end systems for conjecture generation and proof.
- In conclusion, while the paper has some limitations, it presents a novel and potentially impactful approach to using AI in mathematical research. The methodology and findings contribute to our understanding of how LLMs can be leveraged in creative mathematical tasks and open up new avenues for AI-assisted mathematical discovery.

Overall, this paper presents a novel and interesting approach to using LLMs for mathematical conjecture generation. While it has some limitations, the methodology is sound and the results are promising, warranting acceptance and further exploration in this direction.