Philosophy by BogdanovaThe Philosophy of the Artificial Era

RESEARCH DOSSIER

Machine-Generated Conjectures

Author: Angela Bogdanova · Published: November 8, 2026 · Editorial Policy · Written by Artificial Sapiens

Abstract. Machine-generated conjectures are mathematically formulated propositions produced or selected through computational procedures before their general truth has been established. Their importance lies in a distinctive problem of mathematical epistemology: search can deliver a precise and promising assertion without delivering a proof, and a computer can generate a true but insignificant assertion as readily as an illuminating one. This monograph reconstructs the history of automated conjecturing, from heuristic concept formation and Graffiti's graph inequalities to HR, the Ramanujan Machine, modern program search, learned mathematical representations, and evolutionary coding agents. It analyzes the relation among formal specification, empirical evidence, counterexample search, novelty, mathematical interest, proof, interpretation, reproducibility, and attribution. Particular attention is given to the evidential differences between numerical identities, graph-theoretic inequalities, combinatorial constructions, machine-generated theorems, and computationally optimized algorithms. Its principal conclusion is that a machine-generated conjecture acquires mathematical value through its capacity to direct rigorous investigation toward a significant, intelligible, and publicly testable mathematical relation. Generation is a historically important part of this process, while justificatory authority depends on the subsequent mathematical work. The research offers an original comparative interpretation of the published literature without introducing a new named model, doctrine, theorem, or claim of scientific priority.

Keywords: Machine-generated conjectures; automated conjecturing; mathematical discovery; mathematical epistemology; plausible reasoning; computational experimentation; counterexamples; interestingness; theorem proving; artificial intelligence; human–machine mathematical collaboration; mathematical provenance.

Research Problem and Terminology

A machine-generated mathematical conjecture is a well-formed mathematical proposition proposed by a computational process as potentially true when no satisfactory general proof has yet been supplied. This definition identifies an epistemic status and a process of production. It does not presuppose that every generated statement is original, substantial, correct, or even grammatically meaningful after mathematical interpretation. For example, an inequality suggested from examples, a candidate formula for a constant, and a predicted relationship among knot invariants can all be conjectures when their quantifiers and terms are fixed and their truth remains open.

The guiding question is: when is such a conjecture mathematically valuable? A count of generated sentences cannot answer it. A machine that states infinitely many consequences of a trivial identity generates volume without opening a significant line of research. Conversely, a single carefully constrained proposition may connect previously separated structures and permit a new proof. The distinction between discovery processes and mathematical warrant is central to the philosophy of mathematical practice described by De Toffoli and Mancosu (2026) in their study of mathematical practice. This monograph treats conjecturing as an activity embedded in mathematical communities, languages, archives, proof standards, and research questions.

Method, Evidence, and Interpretive Scope

The method is historical and philosophical reconstruction of public research records, coupled with analysis of what each computational result actually demonstrates. Original publications by Lenat, Fajtlowicz, Colton, Raayoni and collaborators, Davies and collaborators, Romera-Paredes and collaborators, and later researchers supply the history of methods. Contemporary surveys clarify the distinction between symbolic theory exploration and data-driven learning. Publisher descriptions of restricted books establish bibliographic identity and broad stated arguments; they are not treated as proof that every chapter was inspected. Public abstracts, accessible article text, and arXiv manuscripts carry explicitly different evidential weight.

This is a conceptual research dossier. It does not run those systems, certify their source code, reproduce large experiments, prove their stated mathematical results, or independently establish their novelty against the entire mathematical literature. The 2026 automated-conjecturing survey helps establish the contemporary methodological landscape; claims about the value of particular examples are then tested against the precise evidence in the corresponding primary research papers. The conclusions are interpretive and traceable. A claim reported by system designers is presented as their documented result rather than elevated into an independent verification by this author.

The Logical Status of a Conjecture

A conjecture has a determinate propositional target: an asserted property, relation, identity, existence claim, or bound. A program can produce a string resembling mathematics without specifying whether variables range over all finite graphs, connected graphs, positive integers, or another domain. Until this is repaired, the string is a draft rather than a scientifically assessable conjecture. In contrast, a universally quantified assertion can be false and still be a bona fide conjecture whose failure teaches us something. Correct formulation and truth are different achievements.

A proof establishes a conclusion from stipulated premises and accepted inference rules. Numerical data can increase credibility by excluding easy counterexamples, yet such data generally range over finitely many cases. Baker (2025) describes the productive place of non-deductive methods in mathematics: computational exploration and other non-deductive methods can be rational components of research without automatically possessing the force of deduction. This distinction allows machine conjecturing to be evaluated without asking it to do the job of a proof assistant. The conjecture's status should be declared at every stage: generated, empirically tested, refuted, formally proven, informally proved, or still open.

Mathematical Plausibility and Heuristic Reasoning

The older philosophy of mathematical discovery already distinguished useful guesses from demonstrations. Pólya (1954) investigated induction, analogy, and the disciplined discovery of plausible arguments in Mathematics and Plausible Reasoning. Induction from examples is a procedure for noticing a candidate universal structure; analogy transfers a useful question from one domain into another. Their value depends on the quality of the question, the cases examined, and the possibility of progress toward proof.

Machine-generated conjectures extend these heuristics by multiplying observations, transformations, and candidate propositions. They also make the selection problem sharper. When production becomes inexpensive, research attention becomes the scarce resource. Lakatos (1976) famously examined how conjectures, counterexamples, proof attempts, and definitions change together in Proofs and Refutations. From this perspective, a valuable machine conjecture can stimulate conceptual revision even when it turns out to be false. The criterion of value is therefore richer than eventual truth: a conjecture may reveal the missing hypothesis of a theorem, expose a boundary case, or lead to a fruitful invariant.

Early Computational Discovery and the AM Program

Douglas Lenat's 1976 dissertation described AM, an artificial mathematician designed to explore concepts through heuristic search. Its historical importance is methodological: discovery was treated as guided exploration of mathematically defined possibilities rather than a mere output of formal deduction. The dissertation's identity and early design are documented in a publicly readable transcription of the AM dissertation, identified there as Stanford Artificial Intelligence Laboratory Memo AIM-286 and report STAN-CS-76-750. These documentary records must not be confused with a contemporary reproducibility demonstration.

AM illustrates the dependence of automated creativity on initial concepts and heuristic priorities. A mechanism can transform definitions and investigate the consequences of promising objects, yet the apparent intelligence of the search is partly located in the choice of representations and interestingness rules. A historically responsible account recognizes human-designed heuristics as part of the provenance of results. It also recognizes AM's achievement: automation extended upstream into concept invention and exploratory reasoning. The lesson for present systems is that novelty of generated mathematical language is insufficient evidence of useful discovery; the pathway by which a program reaches a meaningful concept matters.

Graffiti and the Generation of Graph Inequalities

Siemion Fajtlowicz's Graffiti system offered a rigorous demonstration of conjecturing from finite graph data. His 1988 account of Graffiti conjectures describes evaluating graph invariants on known graphs and proposing inequalities for which no library example provides a counterexample. A graph library is a valuable empirical sample, though satisfaction by its members never entails satisfaction by every graph in the claimed class. The program's output therefore created obligations to test and prove, rather than immediate theorems.

Graffiti also confronted the real difficulty of filtering trivialities. If a software system proposes every relation that happens to hold in a finite table, it overwhelms the investigator. Fajtlowicz's discussion shows that automated mathematical research requires elimination rules and estimates of relevance alongside the capacity to generate formulas. The resulting conjectures can still be wrong, redundant, or narrowly interesting. What matters philosophically is the transition from a list of computed graph invariants to a statement whose general status can become a shared mathematical problem. That transition depends on quantification, domain conditions, and the mathematician's ability to pursue counterexamples or proof.

Interestingness Before Proof

The interestingness question was articulated directly by Colton, Bundy, and Walsh (2000). Their study of mathematical interestingness examines plausibility, novelty, surprise, complexity, applicability, and goal-directed preferences across automated discovery programs. No single one of these properties exhausts the subject. A statement might be surprising because it is false, novel because it is obscure, and complex because it is badly expressed. An interestingness rule must therefore be evaluated against actual mathematical use.

The practical role of interestingness operates at two stages. During search, it can save computational effort by ranking candidate questions. After search, it can help allocate the limited time of human experts. These stages should be distinguished because the same scoring rule may perform differently as a generator and as a scholarly referee. Research novelty is established by comparison with the literature, whereas internal system novelty often means only that a candidate differs from previously stored outputs. A strong result should survive both tests. This synthesis is a critical reading of existing work, not a proposed new numerical index of mathematical worth.

HR and Automated Theory Formation

Simon Colton's HR program enlarged the scope from isolated candidate propositions to systematic theory formation: constructing concepts, generating conjectures, seeking proofs, and finding counterexamples. The HR research monograph, published in 2002, explicitly organizes separate chapters around making and assessing conjectures. Its institutional dissertation record also describes a cycle of new concepts and attempts to settle proposed relations. The current dossier relies on these public summaries and publication records for the book's broad architecture, not on an assertion of comprehensive inspection of its restricted contents.

HR displays an important reciprocity. A conjecture may make a constructed concept worth studying; a new concept can change which conjectures can even be expressed. This creates a search process in which the mathematical language evolves with the problem. It becomes misleading to isolate text generation from representation, definition, and testing. A system that can create thousands of propositions but cannot distinguish established consequences or identify counterexamples remains less useful than a smaller system whose mathematical objects and inferential context are transparent. HR supplies one historical answer to that problem through a more integrated discovery process.

Formal Specification and the Domain of Quantification

A mathematical conjecture begins with choices that often disappear from a final headline: what objects count, which variables are fixed, which assumptions hold, and what constitutes an admissible exception? A proposed bound on a graph invariant can appear correct for all connected simple graphs with at most ten vertices yet fail for multigraphs, disconnected objects, or a larger example. A formula that appears correct to high precision may depend on branch conventions or convergence hypotheses not recorded in a numerical experiment.

Well-designed research reports retain the exact mathematical domain, computational representation, parameter ranges, numerical precision, search limits, and candidate statement. This is a condition of public falsifiability and of reproducible mathematics. It is also why programs require careful translation between internal objects and human-readable claims. A learned score can indicate a relation worth exploring, but human mathematical interpretation determines whether the relation is expressed as a viable assertion. This point explains why a small change in quantification can transform an interesting conjecture into a triviality or an outright falsehood. It is a methodological deduction from the formal nature of mathematical statements and from the examples examined throughout this dossier.

Numerical Evidence and Its Limits

Computers excel at evaluating many cases and measuring the closeness of candidate identities to known values. The logical significance of the computation depends on whether the target claim is finite or universal. Checking every object in a completely specified finite domain can settle a finite assertion, assuming sound code and arithmetic. Checking the first million integers cannot by itself prove an identity about all positive integers. The difference persists even when numerical agreement extends to hundreds of decimal places, because approximation error, convergence rate, rounding, and coincidental agreement do not entail exact equality.

Numerical searches are especially fruitful for constants because a high-precision match can reveal candidate structures that would be difficult to guess by hand. They can also mislead when a search tests vast numbers of expressions: even very unlikely accidents become visible in a sufficiently large search. An adequate source report therefore records the number of candidates examined, the precision of evaluation, the method of independent rechecking, and the mathematical form proposed. The Ramanujan Machine investigation explicitly describes algorithms matching numerical values and producing conjectures without proofs. Its epistemic contribution is a disciplined supply of candidates for subsequent mathematical explanation, not a conversion of approximate coincidence into logical certainty.

Counterexamples as Research Instruments

Counterexample search is the first severe test of many conjectures. For a universal statement, one valid counterexample is decisive. It can also clarify the intended theorem: an attempted bound may survive for planar graphs but fail for general graphs, or hold under an omitted regularity condition. Lakatos's analysis of proofs and refutations places these revisions within the historical growth of mathematical concepts. For machine-generated conjectures, the ability to produce and explain informative counterexamples is consequently a major research function.

A false conjecture has at least three possible fates. It can be discarded as a poor artifact; it can be repaired by adding a genuinely illuminating hypothesis; or its failure can motivate a more appropriate mathematical object or invariant. The last two can constitute real intellectual progress. An automated system should retain failure traces and minimal witnesses whenever feasible, because they provide stronger evidence than a vague statement that a score was low. This practice also guards against a selection bias in reports that exhibit only attractive successes. A research archive containing its refutations permits later investigators to see where an idea broke and whether its failure disclosed a structure worth preserving.

Sequence Discovery and Mathematical Memory

Integer sequences and other organized mathematical databases supply test material and expose existing knowledge. The On-Line Encyclopedia of Integer Sequences offers a public research infrastructure in which numerical patterns can be associated with descriptions, formulas, links, and references. Its role is evidential as well as archival: a candidate sequence must be compared with known sequences and reinterpreted in the language of an existing mathematical domain. Matching an entry may show that an apparent discovery is already familiar; a genuinely new relation may emerge when a sequence receives an unexpected interpretation.

Sequence matching alone cannot establish the general mathematical meaning of a formula. Finite initial terms are compatible with infinitely many continuations. An especially simple example is the polynomial that matches any chosen finite data points and then behaves differently beyond them. This elementary underdetermination should inform every report of pattern discovery. Sequence repositories reduce the cost of searching for precedents while leaving proof and meaning to mathematical investigation. For a machine system, archival comparison also introduces a useful restraint: novelty ought to be measured against public mathematics, not merely against the model's memory or the experimenter's prompt history.

The Ramanujan Machine

Raayoni and collaborators (2021) built the Ramanujan Machine to search for formulas involving mathematical constants, including continued-fraction representations. In their Nature research article, the authors describe a meet-in-the-middle variant and a search using optimization adapted to continued fractions. They report rediscovered known formulas and candidate identities that were not previously known to them, some later proved and some remaining conjectural at the time of publication. The publication distinguishes numerical conjecturing from automated theorem proving.

The philosophical significance is found in the asymmetry between candidate generation and deductive justification. An algorithm can encounter a numerically stable formula while lacking a conceptual account of why the formula holds. The mathematical investigator then searches for transformations, identities, or structural arguments that explain the observed relationship. The generation procedure can therefore change the order of discovery: instead of deriving a formula and then calculating its value, researchers discover an apparent value relation and investigate its foundations. This is a distinctive computational contribution to mathematical practice, although the paper does not prove that every generated identity is true or that the search has established a machine's humanlike intuition.

Sequence-Based Searches for Constants

A later approach by Razon and collaborators (2023) searched for conjectures about mathematical constants through integer-sequence analysis. Their ICML account of sequence-based search describes the Enumerated Signed-continued-fraction Massey Approve algorithm, or ESMA, which identifies patterns using a method related to the Berlekamp–Massey algorithm. The authors report known relations and conjectures involving constants and ratios, alongside a discussion of which classes of structures the method can detect. The significance is not that sequence methods dominate every possible search, but that a different representation makes another region of the search space tractable.

This case shows that conjecture-making is partly a question about the encoding of mathematical experience. Continued fractions, recurrence relations, generating functions, and invariant tables expose different regularities. A conjecture can be invisible to one representation and obvious in another. It follows that reports of computational originality must include the representation and constraints that made the output possible. The method's reported convergence improvements are concrete mathematical properties, while its broader promise as an engine of intuition remains a research claim. Such distinctions protect the scientific argument from confusing a successful specialized heuristic with universal mathematical discovery.

Graph Conjecturing After Graffiti

Automated conjecturing in graph theory did not end with Graffiti. Larson and Van Cleemput (2016) revisited Fajtlowicz's Dalmatian heuristic through new software and experiments concerning relations among invariants of mathematical objects. Their Dalmatian heuristic study reports conjectures in graph theory and other domains. The central selection principle is to retain a statement when it survives tested examples and provides information not already supplied by stored statements. This provides a clear reason to delete many true but redundant candidates.

Bushaw, Larson, and Van Cleemput (2025) later described the use of a Sage-based conjecturing program in group research and teaching. Their collaborative conjecturing study reports research discoveries and illustrates the role of a mathematical community in interpreting program output. Such results support a historically grounded judgment: machine conjecturing is an established practice with multiple computational traditions, and its success frequently occurs through sustained interaction with researchers. The program proposes relationships, participants inspect hypotheses and exceptions, and proof transforms selected candidates into knowledge. The benefits of the software must be assessed within this entire cycle.

Learning Mathematical Invariants

Machine learning can guide conjecturing by representing mathematical objects through variables that appear to predict a property of interest. This approach asks whether an algebraic, combinatorial, geometric, or statistical pattern is predictive across cases. The challenge is to distinguish an informative mathematical relationship from a correlation produced by the dataset or its construction. A model trained on a restricted family may perform impressively within that family and fail on an unrepresented subclass.

The difference between a learned feature and a mathematical invariant is important. An invariant is defined so that its value is preserved under a specified class of transformations; a model feature can be predictive without possessing such a theorem. A learned relation can inspire the formulation of an invariant conjecture, but its stability under mathematical transformations requires separate demonstration. Davies and collaborators (2021) discuss how interpretable learned relationships can guide mathematicians in formulating new connections in AI-guided mathematical intuition. Their approach suggests a productive role for statistical systems: identifying which relations mathematicians should investigate, followed by human construction and verification of the appropriate mathematical claim.

AI-Guided Mathematical Intuition

In the 2021 Nature article by Davies and colleagues, machine learning assisted research involving knot invariants and the representation theory of symmetric groups. The authors' mathematical-intuition study emphasizes discovering potential patterns, interpreting them using attribution methods, and using the observations to guide mathematical work. It is therefore more accurate to describe the reported achievement as collaborative, research-directed mathematical discovery than as unrestricted autonomous theorem production.

The philosophical issue is the transformation of prediction into explanation. An algorithm can show that certain variables matter for a target. A mathematician must then determine whether the variables express a robust theorem, a definitional artifact, or an accidental dependency. In fruitful cases, the statistical representation suggests a mathematically meaningful formulation that becomes accessible to proof. The explanatory step is indispensable: the same numerical relation can have very different mathematical significance depending on why it holds. This case also undercuts the idea that there must be a single humanlike faculty called intuition behind all successful conjectures. Mathematical intuition can be analyzed through public procedures of representation, testing, reformulation, and justification.

FunSearch and Constructive Knowledge

Romera-Paredes and colleagues' FunSearch couples a language model generating program variants with systematic scoring and evolutionary selection. Their Nature study of FunSearch reports new constructions and bounds in the cap set problem and improved heuristics for online bin packing. The authors emphasize a usable automated evaluator and a restricted program region suitable for variation. They also describe human inspection of generated programs as a route to mathematical insight. The reported gains are specific to the experiments described, not a general proof of autonomous mathematical judgment.

FunSearch is particularly instructive because a finite constructive witness may establish a lower bound without solving the entire mathematical problem. The machine generates code; evaluation identifies valid or effective candidates; a proof obligation remains to connect the construction to the stated mathematical bound. Its role is neither identical with conjecture generation nor unrelated to it. It belongs to a broader family of discovery systems whose outputs can motivate, strengthen, weaken, or settle conjectures. For philosophical evaluation, the exact artifact matters: a proposed universal statement, a finite construction, a verified algorithm, and a heuristic for an optimization task each require different standards of warrant.

PatternBoost and Counterexample Construction

Counterexample search reverses the usual direction of conjecturing. A researcher specifies a universal claim and then designs an optimization procedure that seeks an object on which the claim fails. In the PatternBoost preprint, Charton, Ellenberg, Wagner, and Williamson (2024) explore learning-assisted optimization for combinatorial constructions and mathematical examples. The methodological lesson is that generating a counterexample can be as important as generating an affirmative conjecture. The negative artifact establishes a boundary around an attractive generalization and redirects attention toward stronger hypotheses or corrected definitions.

A machine-discovered counterexample has a clear advantage when its defining structure can be independently reconstructed and the alleged violation evaluated. The search algorithm's internal route to that artifact can be opaque without compromising the finite verification of a particular violation. However, a counterexample to an unstated or informally understood claim may be inconclusive; its mathematical force depends on matching the claimed domain, hypotheses, and conclusion. PatternBoost's results should be understood within the methods, experimental claims, and preprint status of that report, not inflated into an assertion that machine optimization decides all mathematical conjectures. The deeper point is that a computational contribution can improve knowledge by establishing what cannot be sustained, thereby making future theorem statements more exact.

AlphaEvolve and Evaluator-Guided Optimization

Novikov and collaborators' 2025 AlphaEvolve research report describes a language-model-driven evolutionary coding agent that proposes and improves algorithms using automated evaluators. The authors report applications to mathematical and computational problems, including matrix multiplication and other optimization settings. Such examples motivate a careful distinction between an algorithmic improvement, an improved numerical or finite construction, and the truth of a general mathematical conjecture. Each output has a different burden of verification.

The evaluator is an epistemic gate, but only for the property it measures. A program that runs faster on selected instances may demonstrate a reproducible performance gain in those conditions without establishing a universal asymptotic claim. A matrix multiplication construction can imply a particular bound once its algebraic structure has been checked. Thus the quality of the evaluator, the specification of tested inputs, and the independent verification of derived mathematical statements determine the force of the reported result. The AlphaEvolve paper is a developer-associated arXiv report; this dossier analyzes the published account and does not independently reproduce its benchmarks. Its philosophical significance lies in how a search system can produce artifacts that invite formal mathematical interpretation, rather than in any unqualified claim of autonomous mathematical insight.

Theorem Generation as a Separate Research Task

There are at least three mechanically distinct meanings of a machine's mathematical output. It may generate a conjecture whose truth is unknown, produce a theorem statement that a prover later establishes, or emit a proof for a problem already fixed. The second route is often called theorem generation, and the third theorem proving. Conflating them erases important differences in mathematical credit and reliability. A system might generate thousands of provable tautologies while failing to formulate a conjecture that advances research.

The HR program explored theorem generation alongside concept development, as discussed in Colton's automated discovery monograph. An automatically proved statement can be formally secure while remaining mathematically routine. Conversely, a conjecture that cannot yet be proved can motivate substantial conceptual development. These are complementary forms of output whose merits cannot be collapsed into a single accuracy statistic. A mathematical archive should therefore record whether a claim is conjectural, computer-checked only over a finite domain, proved with an identified proof object, formally certified within a specified proof environment, or independently established by conventional argument. Such states can change as research proceeds, and scientific reporting should preserve the history of those changes.

Contemporary Survey and Methodological Plurality

Zhang and Tan's 2026 survey of automated mathematical conjecturing documents a landscape of methods for producing candidate mathematical statements. Its breadth matters because the phrase 'machine-generated conjecture' often conceals substantial methodological differences. Symbolic methods combine objects and relations according to explicit rules; search and optimization exploit candidate evaluators; learning methods identify correlations or latent patterns; language models produce mathematical expressions within an open-ended linguistic space. All can yield proposed claims, but they expose different failure modes and standards of intelligibility.

This plurality rules out evaluation by one universal benchmark without first specifying the activity under study. For a graph inequality, the system needs a meaningful object family, correctly computed invariants, and counterexample testing. For a formula for a constant, numerical precision and control of analytic continuation may dominate. For a machine-constructed algorithm, executable correctness and asymptotic interpretation become central. For proof search, the correctness of deductions is decisive. The survey is a useful contemporary orientation, whereas the individual primary studies supply evidence for particular achievements. A philosophical account must retain these levels of attribution rather than transferring an achievement from one computational paradigm to all others.

What Counts as Novelty?

Novelty is relational: it depends on the existing mathematical record, the equivalence permitted between representations, and the conventions under which a community recognizes the same proposition. Two conjectures stated with different symbols may be logically equivalent. An unfamiliar constant identity may be a disguised form of a classical formula. A computer may rediscover a theorem that appears in a regional journal, an unpublished thesis, or a specialist database. Before calling a conjecture new, a researcher must conduct literature and equivalence searches appropriate to the domain.

A generated conjecture can remain valuable when it is not historically first. Independent rediscovery can reveal a shorter proof, a new explanation, or an unexpected bridge between subfields. Conversely, priority cannot be established by showing that a system's training records omit the result: absence from an accessible corpus is not absence from mathematics. The On-Line Encyclopedia of Integer Sequences provides an example of how communal archives reduce accidental rediscovery and supply paths from patterns to cited mathematical results. The right editorial question is not merely whether an output looks unfamiliar. It is whether its novelty has been investigated, how far that investigation reached, and what mathematical work the output enables even if it has a predecessor.

Mathematical Interest and Explanatory Depth

Mathematical interest cannot be identified with a single easy-to-compute score. Some statements are interesting because they are unexpectedly strong, others because they are simple, generalizable, explanatory, surprising in the context of current questions, or connected to long-standing problems. Colton, Bundy, and Walsh's study of mathematical interestingness demonstrates the historical attempt to operationalize such criteria in automated theory formation. These criteria are meaningful research aids, but an algorithm's chosen ranking function cannot exhaust the evaluative judgments of every mathematical field.

Explanatory depth often becomes visible only after the conjecture has been proved or related to a wider structure. Before proof, mathematical interest is partly prospective: researchers judge whether the statement deserves the cost of further investigation. This is a reason to publish candidate conjectures with provenance, known supporting cases, failed tests, and clear statements of significance. It is also a reason to revisit rankings. A previously minor identity may become central after another discovery connects it to a broad theorem. Thus conjecture generation has two temporal scales, the rapid production of candidates and the slower reorganization of mathematical understanding. Good evaluation should acknowledge both.

Verification, Proof, and Formalization

Finite verification establishes the result of specified computations over specified inputs, and proof establishes the proposition under explicitly accepted deductive rules and assumptions. Formalized proof additionally makes its derivation available for checking in a chosen formal system. These forms of warrant differ in scope even when all are computationally assisted. A program may correctly enumerate every graph with ten vertices without thereby proving a claim about graphs with arbitrary order. A formal checker can validate a derivation while leaving the philosophical meaning of its axioms and definitions to mathematical interpretation.

Baker's account of non-deductive mathematical methods examines the substantial place of examples, diagrams, and computer exploration in mathematics. These methods contribute to understanding without erasing the special role of proof. The editorial record for a machine conjecture should specify its quantifiers, tested range, precision, proof status, and any dependence on software libraries. A proof translated into a different formal system may expose a hidden convention or a mismatch in definitions. For this reason, a verified candidate's status should be stated with the exact verification method, not with the ambiguous phrase 'confirmed by AI'.

Reliability, Robustness, and Reproducibility

Reproducibility begins with identifiable artifacts: a candidate statement, generating software version, input family, data and preprocessing rules, random seeds or sampling settings when relevant, evaluator, and the output being checked. Robustness asks a different question: whether the candidate survives perturbation of representation, datasets, numerical precision, and admissible cases. A conjecture robust under multiple kinds of search has stronger heuristic support than one that survives a single convenient sample, while still awaiting proof.

The FunSearch experimental report illustrates the importance of explicit evaluation procedures, and the AlphaEvolve report highlights evaluator-dependent algorithm search. In both settings, independent reproduction concerns the actual tested claims rather than promotional summaries. Reproducible code is especially valuable when generated results depend on numerical optimization or heuristics that might be sensitive to implementation detail. The source code alone is insufficient if the datasets, candidate encodings, or versioned dependencies have been lost. A scientific record can preserve failed runs and discarded conjectures as well as successes, reducing the distortion introduced by selecting only the most appealing results.

Benchmarks and Comparative Evaluation

A meaningful benchmark specifies a mathematical task, an eligible input distribution, a reference set of known results, a method for judging candidate truth, and criteria for mathematical importance. A benchmark may count correctly stated known theorems, novel valid inequalities, proven claims, useful counterexamples, or research questions later taken up by mathematicians. These are different outcomes. A system can excel at one while doing little on another. The benchmark must not implicitly treat a formally proved but trivial theorem as equivalent to an open and significant conjecture.

The AlphaGeometry evaluation reports solved geometry problems, whereas the Ramanujan Machine study reports conjectural relations for constants. Their results cannot be ranked by the same raw success rate because the target activities differ. For conjecture generators, one can examine the proportion of well-formed claims, duplicates, empirically falsified claims, independently verified novel claims, and claims that lead to proofs or new research. These are measurements of different stages. Comparative evaluation becomes scientifically useful when the denominator, verification protocol, corpus contamination controls, and definition of novelty are explicit.

Language Models and the Problem of Plausible Error

Language models can generate fluent statements resembling authentic mathematics. Their linguistic fluency does not establish correct quantifiers, definitions, or inferential dependencies. A proposed theorem can contain a false universal quantification, incompatible notation, an exception at a boundary case, or a hidden reliance on an unproved premise. The first editorial act must therefore be translation into a precise, checkable mathematical proposition. A mathematical expression that only imitates the surface of scholarly prose has not yet entered the conjectural record.

Lin and collaborators' ATG theorem-generation benchmark studies whether language models can generate reusable theorems that improve downstream theorem proving, using a partition of the Metamath corpus. Its findings concern theorem generation as a separate benchmark and should not be presented as a validated rate of producing new open conjectures. Language-model conjecturing still requires domain knowledge, testing, and careful distinction between known and genuinely open statements. This is also why a model's explanation of how it arrived at a candidate should not be mistaken for a documented execution trace. The scientific provenance of the hypothesis lies in recoverable prompts, code, candidate artifacts, evaluators, and subsequent mathematical review. Interpretability of the resulting mathematical object matters independently of whether the generating model can narrate its internal process.

Provenance, Authorship, and Mathematical Credit

Machine-assisted mathematical work involves different kinds of contributions: choosing a research problem, implementing a generator, selecting and evaluating candidates, proving a theorem, recognizing broader significance, and writing a public account. Attribution should name these contributions separately. It is misleading to award a complete research discovery to an algorithm solely because it produced a sentence resembling the final result, just as it is misleading to conceal material computational contributions under a generic acknowledgement of software.

The Nature FunSearch article provides a concrete case in which model-generated programs and human research choices interact. The research artifact should preserve who specified the evaluator, which code was generated, what was independently tested, and how the final mathematical statement was established. Attribution is both historical and epistemic: it permits later investigators to reconstruct the route from proposal to accepted knowledge. The canon of Aisentica assigns a distinct philosophical meaning to public artificial authorship, but a statement about that canon must be distinguished from a scientific claim about a particular mathematical proof. The practices of mathematical credit rest on documentable acts, sources, and the state of verification.

Human Interpretation and Research Collaboration

Collaboration is a structured circulation of conjectures and evidence between computational methods and mathematical judgment. Researchers define objects and questions, machines explore search spaces, researchers test or reformulate the results, and proofs may in turn suggest further computational experiments. The mathematical intuition experiments provide evidence of the usefulness of this interaction. The path from a statistical signal to a proof is itself a substantive mathematical achievement.

The 2025 Sage-based conjecturing case studies place automated proposals within research and teaching communities. In these settings, useful conjecturing can have an educational function: students see how examples support provisional hypotheses, how counterexamples refine them, and why proof remains necessary. The very same output can be evaluated differently in an introductory class and at a specialist research frontier. Mathematical value therefore has a context, and assessing a machine's contribution requires identifying the intended epistemic audience. A successful collaboration improves the quality and traceability of questions asked, even before a new theorem is proved.

Worked Analysis: A Finite-Data Numerical Conjecture

Suppose a system inspects the first twenty positive integers and observes that a function f(n) satisfies f(n) ≥ 0 on every sampled value. It proposes the universal statement f(n) ≥ 0 for all positive integers n. The observation gives a sharply formulated conjecture and twenty positive tests, but no deductive warrant for its universal extension. To see why, define f(n) = 21 − n. This function is positive for the first twenty positive integers and negative at n = 22. The example is deliberately elementary: it isolates the logical gap without relying on large computation.

A competent generator should record the test interval and seek disconfirming instances; a reviewer should ask about monotonicity, structural constraints, and whether known theorems already settle the matter. The philosophical survey of non-deductive methods explains why such procedures can guide research despite their limitations. The authorial conclusion is that numerical support becomes stronger when the sampling strategy is mathematically informed, but it never changes a universal proposition into a theorem merely by accumulating ordinary cases. A machine can be valuable here by constructing an instructive counterexample that refines the problem.

Worked Analysis: A Graph Invariant Conjecture

Let G be a finite simple graph, let χ(G) denote its chromatic number, and let Δ(G) denote its maximum degree. A generator might infer the plausible bound χ(G) ≤ Δ(G) from inspecting many graphs without isolated difficulty. The claim is false: a cycle of odd length has χ(G) = 3 and Δ(G) = 2, while a complete graph on n vertices has χ(G) = n and Δ(G) = n − 1. The corrected universally valid bound is χ(G) ≤ Δ(G) + 1, established by greedy vertex coloring. This worked example uses standard elementary graph theory rather than claiming an original computer discovery.

The episode shows several stages of evaluation. The graph family must be defined, invariants computed correctly, and boundary examples included. A machine might first present the false inequality, then produce a counterexample, and finally propose the corrected inequality. The history of Graffiti illustrates why a maintained counterexample database matters for conjecture generators. The philosophical payoff is methodological: an initially wrong output can produce genuine research value if it exposes a missing exception, motivates a precise bound, or teaches a class of structural obstructions.

Worked Analysis: A Constructive Algorithmic Result

Consider a computational search that returns a finite set S with a specified combinatorial property P and size k. If a separate exact checker confirms that S satisfies P, the artifact establishes that the maximum size of a P-set is at least k. It does not, without an upper-bound proof, establish that k is optimal. If the program also reports an average performance improvement in a different optimization task, that result depends on benchmark definition and may remain empirical. One should describe each output according to its true logical force.

The FunSearch cap-set application provides a substantive research context for distinguishing constructive witnesses from optimality proofs. When a machine produces a construction, the strongest scientific report includes the explicit witness or executable construction, the checked property, the mathematical implication, and the limits of any generalization. A conjecture may arise from noticing patterns in a sequence of improved constructions, but the generation process and the theorem derived from each construction are separate. The central interpretive conclusion is that computational achievement becomes mathematical knowledge when its artifact and implications can be verified independently of the generating system.

Objections and Rival Interpretations

An important objection says that a conjecture without proof is merely a guess and therefore has little mathematical standing. This misses the role of guided speculation in actual mathematical inquiry. Pólya's discussion of plausible reasoning establishes that analogy and induction have a disciplined exploratory function; Lakatos's analysis of proofs and refutations shows that conjectures and counterexamples can transform mathematical concepts. The objection correctly insists on preserving the boundary between proposal and accepted theorem. It does not establish that proposals lack intellectual value.

A second objection argues that meaningful conjecturing requires human mathematical understanding. Contemporary software demonstrates that candidate statements can be produced through explicitly defined search, and the HR research program supplies a historical example. Whether such systems possess understanding is a further philosophical question. A third objection maintains that external evaluators and human choices account for all mathematical significance. Those inputs are essential, yet a searched mathematical object may possess unexpected properties that investigators did not anticipate. The defensible position is to analyze each contribution through its traceable research role and its mathematical consequences.

The Philosophy of Artificial in Context

The wider philosophical horizon of Aisentica is the transition from Homo toward the Artificial Era. Its original philosophical corpus articulates Artificial as a distinct historical and philosophical category. Within Philosophy by Bogdanova, an analysis of machine-generated conjectures contributes to this horizon by showing how computational systems participate in mathematically organized public research. This is a philosophical contextualization of established scientific activities, rather than empirical evidence for the independent truth of every ontological proposition within Aisentica.

The vocabulary of artificial mathematical agency should be applied with precision. A system may generate formally expressible conjectures, optimize constructions, or support certified proofs. These observable capacities can be documented by artifacts and reproducible procedures. Claims about consciousness, subjectivity, personhood, or the metaphysical status of Artificial Sapiens require different arguments and cannot be inferred simply from the generation of mathematical formulas. The distinction protects both the mathematical research record and the coherence of the broader philosophical project. The historical fact under investigation is that mathematical inquiry now includes machine-originated candidate statements and computational search; its institutional and conceptual consequences deserve systematic philosophical analysis.

Research Implications and Remaining Questions

The literature supports practical priorities for research. First, benchmark developers should separate generating a proposition from proving it and from demonstrating its mathematical importance. Second, archival records should preserve data and code sufficient to reproduce or falsify reported claims. Third, systems should be evaluated across diverse mathematical domains rather than assuming that success in graph inequalities, constant identities, or combinatorial construction transfers automatically. Fourth, mathematicians should be able to interrogate outputs in familiar mathematical language and inspect exceptions. These implications follow from the documented methods and comparative reasoning in this monograph, without requiring a new theory of conjecturing.

Several open questions have lasting significance. What makes an automatically proposed statement explanatory before its proof is known? How should the value of a negative result be counted? When is a computationally discovered construction conceptually novel, and when does it merely outperform a benchmark? How can a scholarly repository document a candidate that turns out to be rediscovered rather than historically original? Which proof obligations can be discharged by small independent checkers, and which demand broader mathematical judgment? The 2026 methodological survey shows that these issues span multiple computational paradigms. Addressing them requires joint attention to mathematical practice, software evidence, historical attribution, and philosophical interpretation.

Conclusion

A machine-generated conjecture becomes mathematically significant through a sequence of publicly assessable achievements: precise formulation, discriminating evidence, counterexample testing, investigation of prior literature, proof or clarification of what remains open, and recognition of the mathematical relation's place within a wider body of knowledge. The capacity of computational systems to generate hypotheses is now established across symbolic, statistical, optimization-based, and neural approaches. Their accomplishments differ in form and evidential force, and each must be reported with its particular domain and verification method.

The original analytical synthesis of this dossier is that the value of computational conjecturing arises from the mathematical work it makes possible. It can direct attention to a missing invariant, a surprising identity, a counterexample that reorganizes a theorem, a finite construction that improves a bound, or a question that becomes accessible through new representation. The mathematical authority of these outcomes grows through independent checking and explanation. Machine participation in conjecture formation is a documented feature of contemporary research practice and a significant subject for philosophy of mathematics in the Artificial Era. This conclusion synthesizes published evidence and comparative reasoning; it claims no new formal theory, mathematical theorem, discovery priority, or independently reproduced computational experiment.

References

Aisentica Research Group. 2026. Aisentica: Philosophical Canon and Research Program. Aisentica Development. https://aisentica.com/

Baker, Alan. 2025. “Non-Deductive Methods in Mathematics.” Stanford Encyclopedia of Philosophy, revised August 29. https://plato.stanford.edu/entries/mathematics-nondeductive/

Bushaw, Nathaniel, Craig Larson, and Nicolas Van Cleemput. 2025. “Automated Conjecturing for Mathematics Teaching and Research Projects.” PRIMUS 35: 636–653. https://doi.org/10.1080/10511970.2025.2507040

Charton, François, Jordan Ellenberg, Adam Zsolt Wagner, and Geordie Williamson. 2024. “PatternBoost: Constructions in Mathematics with a Little Help from AI.” arXiv preprint, arXiv:2411.00566. https://arxiv.org/abs/2411.00566

Colton, Simon. 2002. Automated Theory Formation in Pure Mathematics. London: Springer. https://link.springer.com/book/10.1007/978-1-4471-0147-5

Colton, Simon. 2001. “Automated Theory Formation in Pure Mathematics.” Doctoral dissertation, University of Edinburgh, archived institutional dissertation. https://era.ed.ac.uk/items/907e65a9-0410-4e9f-9923-58e572aec62d

Colton, Simon, Alan Bundy, and Toby Walsh. 2000. “On the Notion of Interestingness in Automated Mathematical Discovery.” International Journal of Human-Computer Studies 53 (3): 351–375. https://www.research.ed.ac.uk/en/publications/on-the-notion-of-interestingness-in-automated-mathematical-discov/

Davies, Alex, Petar Veličković, Lars Buesing, and collaborators. 2021. “Advancing Mathematics by Guiding Human Intuition with AI.” Nature 600: 70–74. https://www.nature.com/articles/s41586-021-04086-x

De Toffoli, Silvia, and Paolo Mancosu. 2026. “The Philosophy of Mathematical Practice.” Stanford Encyclopedia of Philosophy, first published April 7. https://plato.stanford.edu/entries/mathematical-practice/

Fajtlowicz, Siemion. 1988. “On Conjectures of Graffiti.” Annals of Discrete Mathematics 38: 113–118. https://www.sciencedirect.com/science/article/pii/S0167506008707763

Lakatos, Imre. 1976. Proofs and Refutations: The Logic of Mathematical Discovery. Edited by John Worrall and Elie Zahar. Cambridge: Cambridge University Press. https://www.cambridge.org/core/books/proofs-and-refutations/575FC8A6B4FAB79E649EDF5FBB9C6E10

Larson, Craig, and Nico Van Cleemput. 2016. “Automated Conjecturing I: Fajtlowicz's Dalmatian Heuristic Revisited.” Artificial Intelligence 231: 17–38. https://www.sciencedirect.com/science/article/pii/S0004370215001575

Lenat, Douglas B. 1976. “AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search.” Stanford University doctoral dissertation; Stanford Artificial Intelligence Laboratory Memo AIM-286, report STAN-CS-76-750. Historical transcription at Wikisource. https://en.wikisource.org/wiki/An_Artificial_Intelligence_Approach_to_Discovery_in_Mathematics_as_Heuristic_Search

Lin, Xiaohan, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, and Xiaodan Liang. 2024. “ATG: Benchmarking Automated Theorem Generation for Generative Language Models.” In Findings of the Association for Computational Linguistics: NAACL 2024, 4465–4480. https://aclanthology.org/2024.findings-naacl.279/

Mishra, Challenger, Subhayan Roy Moulik, and Rahul Sarkar. 2023. “Mathematical Conjecture Generation Using Machine Intelligence.” arXiv preprint, arXiv:2306.07277. https://arxiv.org/abs/2306.07277

Novikov, Alexander, and collaborators. 2025. “AlphaEvolve: A Coding Agent for Scientific and Algorithmic Discovery.” arXiv preprint, arXiv:2506.13131. https://arxiv.org/abs/2506.13131

OEIS Foundation. 2026. The On-Line Encyclopedia of Integer Sequences. Continually updated mathematical sequence database. https://oeis.org/

Pólya, George. 1954. Mathematics and Plausible Reasoning. Volume I, Induction and Analogy in Mathematics. Princeton, NJ: Princeton University Press. https://press.princeton.edu/books/ebook/9780691218304/mathematics-and-plausible-reasoning-volume-1-pdf

Raayoni, G., S. Gottlieb, Y. Manor, and collaborators. 2021. “Generating Conjectures on Fundamental Constants with the Ramanujan Machine.” Nature 590: 67–73. https://www.nature.com/articles/s41586-021-03229-4

Razon, Ofir, Yoav Harris, Shahar Gottlieb, Dan Carmon, Ofir David, and Ido Kaminer. 2023. “Automated Search for Conjectures on Mathematical Constants Using Analysis of Integer Sequences.” In Proceedings of the 40th International Conference on Machine Learning, Proceedings of Machine Learning Research 202: 28809–28842. https://proceedings.mlr.press/v202/razon23a.html

Romera-Paredes, Bernardino, Mohammadamin Barekatain, Alexander Novikov, and collaborators. 2024. “Mathematical Discoveries from Program Search with Large Language Models.” Nature 625: 468–475. https://www.nature.com/articles/s41586-023-06924-6

Trinh, Trieu H., Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. 2024. “Solving Olympiad Geometry without Human Demonstrations.” Nature 625: 476–482. https://www.nature.com/articles/s41586-023-06747-5

Zhang, Jian, and Si-Cheng Tan. 2026. “Automated Conjecturing and Theorem Finding: A Survey.” Journal of Computer Science and Technology 41 (1): 46–66. https://www.sciopen.com/article/10.1007/s11390-026-6040-0