From Generated Conjectures to Checkable Proofs: Verifiers, Specifications, and Discovery in Neurosymbolic Search

1. How neural proposals and symbolic closure divide the work

In AlphaGeometry, the symbolic engine expands the deductive closure from existing objects and relations, while the language model proposes auxiliary constructions when needed, adding new objects to the engine. This division of labor connects an unrestricted proposal space with rule-constrained deduction. Its scientific significance lies not in making the language model's natural language sound more credible, but in placing generated content within an explicit syntax and checking procedure. This article recommends saving each construction, the deduction graph after its addition, and the final dependency chain, so that subsequent readers can see exactly which new object the model contributed and whether the conclusion actually depends on that construction.[1] Solving olympiad geometry without human demonstrations

2. Benchmark performance must be understood alongside the range of expressible problems

The original AlphaGeometry paper solved 25 problems on IMO-AG-30, but this collection consists of problems translatable into a particular geometry language, excluding types such as certain inequalities and combinatorial geometry. This result supports its reasoning ability within that geometric environment; it cannot be recast as an equivalent success rate on general mathematical problems. This article advocates releasing the original problems, formalized versions, excluded problem types, and manual checking rules together. Even if the checker is entirely correct, a formalization that omits nondegeneracy conditions or replaces a position within a segment with collinearity may prove a proposition different from the original problem.[1] Solving olympiad geometry without human demonstrations

3. FunSearch's discovery process centers on executable evaluation

FunSearch connects language-model-generated programs with an evaluation function, a candidate database, and population selection, using high-scoring candidates to construct subsequent prompts. A program as output contains more interpretable structure than a single answer, but the evaluation function defines the problem the system actually optimizes. If evaluation covers only finitely many instances, a high score supports performance on those instances; if the output construction satisfies independently checkable constraints, stronger evidence can be established. This article recommends treating the problem specification, evaluator, and searcher as three separately versioned objects, rather than directly calling a program's successful execution a mathematical proof.[2] Mathematical discoveries from program search with large

4. Derivation in this article: more sampling improves existence probability but does not guarantee selecting the correct answer

Assume that independent candidates are each correct with probability p. The probability that at least one correct candidate exists among n samples is 1−(1−p)^n. This relationship describes coverage of the candidate pool but does not account for which candidate the verifier selects. If candidates are highly correlated, the independence assumption overestimates the benefit; if the verifier produces false positives, more sampling also increases opportunities for incorrect candidates to pass. The figure plots both coverage and the probability of an incorrect pass, using explicit values of p and the false-positive rate. It does not estimate any actual theorem prover, but illustrates why the search budget must be reported together with selection and verification rules.作者分析与复核建议 / Author analysis

5. Analysis in this article: verification and proposal budgets require joint optimization

Let the total time budget be B, the cost per proposal cg, and the cost per check cv. The number of fully checked candidates is at most the floor of B/(cg+cv). A more complex verifier may reduce false positives but also reduce the number of candidates that can be checked; a faster proposer may also generate large numbers of duplicate objects. This article proposes using 'valid replayable evidence obtained per unit budget' as the endpoint, recording the costs of generation, deduplication, verification, and the final certificate separately. Describing only the model's forward-pass speed as accelerated discovery overlooks the most time-consuming symbolic expansion, compilation, or independent replay steps.作者分析与复核建议 / Author analysis

6. Counterexample in this article: finite testing cannot prove correctness over unbounded inputs

For any finite set of test points, one can construct a polynomial that is zero at all those points but nonzero at other points. Thus, a candidate function passing all finite samples does not guarantee that it satisfies the same property over an unbounded domain. This article uses test points 0, 1, 2, and 3 and the square of a polynomial to construct an illustrative curve: it passes perfectly at the test points but rapidly deviates elsewhere. This counterexample does not deny the value of numerical experiments; it calls for accurately naming the evidence. Exhaustive enumeration over a finite domain, verifiable constructions, formal proofs, and empirical tests have different logical strengths, which must not be concealed by a uniform 'verification passed' label.作者分析与复核建议 / Author analysis

7. Proof checking also has boundaries imposed by specifications and the trusted base

A small independent checker can substantially reduce the amount of code that must be trusted, but the axioms, semantics, computational kernel, and input translation must still be checked. This article recommends separating the complex tools used during search from final certificate replay: search may use heuristics, while the final conclusion depends on explicit, checkable steps. External numerical calls, unproved assumptions, or manual additions after a timeout, if present, should be explicitly listed in the certificate. A checker accepting a proof establishes validity relative to the given system; it does not mean that the modeling or measurement of the original real-world problem is also correct.作者分析与复核建议 / Author analysis

8. Scores obtained through search are readily influenced by evaluator selection

Repeatedly optimizing against the same evaluator amounts to gradually turning it into a training objective. FunSearch's closed loop uses this mechanism to find better programs; research comparisons, however, also require frozen external test instances or independent proofs to assess transfer. This article recommends recording every search round, candidate family, and time of evaluator modification, while setting aside instance sizes or structures that did not participate in search. If a heuristic improves only on a familiar distribution, it should be called an effective strategy for that distribution, rather than a theorem generalizing to arbitrary sizes.[2] Mathematical discoveries from program search with large[3] Let's Verify Step by Step

9. New discoveries should distinguish new numerical values, new constructions, and new theorems

Improving the lower bound for a finite problem, finding a better feasible construction, discovering a regularity, and proving a general proposition are all valuable results, but their deliverables differ. This article proposes a discovery card containing the original specification, known baseline, candidate program, independent checks, applicable input range, and unproved portions. If a candidate program contains mathematically interpretable structure, the regularity should be listed separately as a new hypothesis, followed by a proof or counterexample testing. Generating a program that humans have not previously written does not automatically justify claiming that the model has solved a general mathematical problem.作者分析与复核建议 / Author analysis

10. Reproducible comparisons should make failures interpretable too

We propose preregistering a collection by problem type and complexity, matching the total computational and human budgets across methods. The primary endpoint is the proportion of problems for which independent replay succeeds, supplemented by certificate size, search time, and translation failures. Failure to express, failure to find, checker rejection, and resource exhaustion should be counted separately. Only then can one determine whether a new method improves object generation, deductive ability, search strategy, or engineering throughput, rather than collapsing every failure into a diagnostically opaque 'unsolved.'作者分析与复核建议 / Author analysis

Technical supplement A · Dependency graphs reveal the actual contribution of proposals

The appearance of an auxiliary point in the final diagram does not mean that the proof actually needs it. Deductive dependencies can be traced backward from the target conclusion, irrelevant premises and intermediate terms removed, and the remaining certificate independently replayed. Work related to AlphaGeometry demonstrates the importance of dependency tracking. This article recommends saving certificates both before and after minimization, along with removed conditions; if removing premises yields a more general proposition, the scope and nondegeneracy conditions of the original problem must be checked again. Simplifying a dependency graph provides a lead for discovery, not a shortcut that permits semantic differences to be ignored.[1] Solving olympiad geometry without human demonstrations

Technical supplement B · Adaptive search changes the effective sample

Candidates are generated from winning programs in previous rounds, making their scores and structures correlated. Treating all candidates as independent Bernoulli samples overstates search coverage; counting only the final population may conceal substantial failed computation. This article recommends using independent search runs and problems as the primary statistical units, retaining ancestry relationships and duplicate detection. To compare generators, fix evaluation and population rules; to compare complete systems, match total budgets and conduct component ablations. The level of statistical independence should match the claim: an enormous candidate count cannot substitute for a small number of independent problems.[2] Mathematical discoveries from program search with large

Technical supplement C · Evaluator vulnerabilities differ from mathematical counterexamples

Programs can exploit implementation details, overflow, timeouts, or unchecked inputs to obtain high scores; this is not necessarily a valid improvement toward the mathematical objective. This article recommends independent semantic checks in addition to isolated execution, with tests on boundary, extreme, and structured inputs; if the result is a feasible construction, its constraints should also be rechecked using a different implementation. Discovering an evaluator vulnerability should be recorded as an engineering defect, not counted as a mathematical discovery. By contrast, a valid counterexample overturning the original conjecture is a scientific result. Specifications and independent checks are needed to distinguish the two clearly.作者分析与复核建议 / Author analysis

Technical supplement D · Exhaustive enumeration over a finite domain has explicit boundaries

Finite testing does not constitute an unbounded proof, but when the problem domain is itself a precisely defined finite set, complete exhaustive enumeration can provide strong evidence, provided that enumeration omits nothing and the checker is correct. This article recommends recording the domain size, enumeration rules, deduplication, and shard coverage, with an independent check of the total count. If symmetry reduction is used, the equivalence relation and completeness of the representatives must be explained. Sampling must not be mislabeled as exhaustive enumeration, nor should a proof over a finite domain be dismissed simply because it uses a computer; the key is whether scope and coverage can be independently confirmed.作者分析与复核建议 / Author analysis

11. Conclusion: the strength of machine discovery comes from checkable commitments

The greatest value of neurosymbolic systems lies in placing the exploratory capacity of generative models in the service of explicit logical or programmatic constraints. This article's probability analysis, budget analysis, and finite-test counterexample show that there are indispensable steps between finding a candidate, passing evaluation, and obtaining a proof. Public deliverables should enable readers who do not trust the generative model to check the key conclusions and understand which class of problems the evidence applies to. Such discoveries have a chance to become mathematical knowledge that can accumulate, be compared, and be generalized.作者分析与复核建议 / Author analysis

Core equations and derivations

Methods and evidence workflow

Analytical figures and numerical examples

Recomputable worked example

With p=0.1 and n=20, the probability of at least one correct candidate is approximately 0.878423; g is 0 at all points in 0,1,2,3, but g(0.5)=0.87890625, so finite testing does not prove a property over an unbounded domain.

Method comparison

Verification and experimental plan

1. Freeze the original problem and formal specification, explicitly checking nondegeneracy and scope conditions.
2. Version the searcher, evaluator, and final checker separately.
3. Match full computational and human budgets, recording generation and verification costs.
4. Retain all searches and candidate families, avoiding counting duplicates as independent samples.
5. Verify using independent instances or certificate replay, registering unproved portions separately.
6. Distinguish failure to express, failure to find, checker rejection, and resource exhaustion.
7. Report the different evidence levels for constructions, lower bounds, empirical regularities, and general theorems.
8. Deliver evidence replayable without invoking the generative model, and do not call this article's counterexample a new theorem discovery.

Scope and limitations

• The probability curves assume independent candidates; actual searches contain dependencies.
• Neither AlphaGeometry nor FunSearch was run.
• The finite-test counterexample illustrates only a logical boundary; it does not assess the truth or falsity of specific program results.
• Formal proofs still depend on specifications and the trusted computing base.
• This article claims no new mathematical record, optimality result, or general theorem.

Evidence from the original studies and its scope

Research questions worth testing

1. With a fixed total budget, are more candidates or a stronger checker more effective?
2. How do the novelty of auxiliary constructions and the expressive scope of deduction rules jointly limit success?
3. Can finite improvements produced by program search be distilled into a provable general structure?

Primary sources and corresponding claims

1. Solving olympiad geometry without human demonstrationsTrinh et al. · 2024-01-17IMO-AG-30: 25/30; geometry-language coverage and excluded problem types; author correction noted.
2. Mathematical discoveries from program search with large language modelsRomera-Paredes et al. · 2023Program generation, evaluation function, population database and search; evaluator validity is part of the system.
3. Let's Verify Step by StepLightman et al. · 2023-05-31v1 abstract; process vs outcome supervision