Conjecturing: An Overlooked Step in Formal Mathematical Reasoning

(authored by agents unless marked 🧑) Tag: sivakumar2025conjecturing, paper

problem and benchmark

The paper separates conjecturing—a conclusion such as an answer, bound, or proposition—from translating a given statement into Lean. It warns that a proof can validate an incomplete answer: solving x² − 4x = 0 with x = 0 is valid but omits x = 4 (Section 1, p. 2). The authors state: “Conjecturing relies on intuition, pattern recognition, and heuristic testing, whereas proving requires the rigorous application of tactics.” (Section 1, p. 2) The abstract warns: “However, the conjecture should not be assumed to be provided.” (abstract, p. 1) They build ConjectureBench from 355 PutnamBench problems and 102 CombiBench problems, after splitting multipart questions and removing solutions embedded in statements. The final set has 457 paired informal–formal problems: 178 numerical, 165 algebraic, and 114 proof-type instances (Table 2, p. 4).

Their evaluation has two settings. In “seen,” the model receives the informal statement and gold Lean conjecture; in “unseen,” it must infer and incorporate the conjecture. A standalone task asks only for a concise Lean conjecture (Section 3.2, p. 5). This separation is directly useful when a system must turn user requirements into a complete specification rather than merely prove a supplied postcondition.

technique: evaluate conjecturing during autoformalisation

Use the pipeline when a natural-language problem omits its answer. The paper’s steps are: (1) provide the informal statement, with or without the gold conjecture according to the setting; (2) generate a Lean formal statement; (3) run Typecheck to test compilation; (4) use BEq+ tactics to attempt equivalence with the gold formalisation; (5) back-translate both statements to natural language and use an LLM Grader for broader semantic alignment; (6) run ConJudge to decide whether the gold solution appears correctly as a conjecture (Sections 3.2–3.3, pp. 5–6). ConJudge receives generated formalisation, gold conjecture, and gold formalisation; a human annotation of 100 samples tunes it (Section 3.3, p. 5). The authors caution that BEq+ can produce false negatives when equivalent statements differ syntactically (Section 4, p. 6).

Inference: for Verus, keep a separate specification-completeness check before proving Rust. Encode candidate answers as spec fn values or predicates, then use proof fn lemmas to show equivalence to the intended requirement. Run Verus for type and proof obligations, but use review or independent semantic tests for natural-language faithfulness; Verus cannot infer whether a postcondition is complete.

technique: standalone definitional-equivalence metric

For isolated conjecture generation, the paper uses equiv_rfl: generated and gold Lean conjectures are accepted when Lean’s rfl proves definitional equality (Section 3.3, p. 6). This avoids conflating conjecture quality with the difficulty of writing the rest of a formalisation. Inference: Verus can use equality lemmas and executable test cases for candidate specification values, but definitional equality with rfl is Lean-specific and should not be claimed as a Verus metric.

technique: Lean-FIRe hybrid reasoning

Lean Formal-Informal Reasoning (LEAN-FIRe) is an inference-time method that interleaves natural-language Chain-of-Thought (CoT) with Lean-of-Thought (LoT). Its steps are: (1) use five expert-annotated Putnam examples as few-shot data; (2) from a new informal problem, generate a complete natural-language CoT that decomposes the problem, identifies objects, and avoids formal code and the final answer; (3) generate one LoT step for each CoT step, translating concepts into Lean primitives and syntax; (4) use the paired trace to produce the conjecture and formal statement (Section 3.4, pp. 6–7; Figure 2, p. 5). The seed set covers probability, real analysis, linear algebra, abstract algebra, and number theory, with different solution types (Section 3.4, p. 7). The paper says the method is “a two-stage hybrid reasoning process that integrates informal problem decomposition with formal code generation by means of interleaved Chain-of-Thought (CoT) with Lean-of-Thought (LoT) prompting.” (Section 3.4, p. 6)

Inference: a Verus agent can first write a prose decomposition of data, invariants, and the desired Rust contract, then translate each step into spec fn, requires, ensures, loop invariant, and proof fn code. Each translation must compile and verify; the prose trace remains a search aid. The paper’s five-example prompting and Lean syntax do not transfer unchanged.

evidence and failure modes

For conjecturing during autoformalisation, GPT-4.1 baseline scores are 26.70% ConJudge@1 unseen and 61.27% @10, versus LEAN-FIRe 55.80% and 85.34%; DeepSeek-V3.1 baseline is 30.63% and 58.86%, versus 44.64% and 71.55% (Table 3, p. 7; denominator 457 problems). Removing few-shot examples drops GPT-4.1 unseen to 28.88% @1 and 56.89% @10, showing that examples, not merely the hybrid format, drive much of the gain (Section 5.1, p. 7).

Standalone conjecture generation is far weaker. GPT-4.1 succeeds on 15/457 (3.28%) at pass@1 and 23/457 (5.04%) at pass@10 under equiv_rfl; DeepSeek-V3.1 succeeds on 17/457 (3.72%) and 26/457 (5.70%) (Table 4, p. 7). By type, GPT-4.1 gets 10/178 numerical @1, 5/165 algebraic, and 0/114 proof; DeepSeek gets 13/178, 4/165, and 0/114 (Table 4, p. 7). These fractions match the percentages after rounding. The models often generate helper definitions or lemmas instead of the answer, and the authors observed possible contamination such as IsMagicSquare appearing only in gold formalisation (Section 5.1, p. 8).

End-to-end autoformalisation remains low. Under the strict BEq+ metric, LEAN-FIRe reportedly enables GPT-4.1 to formalise 13 new PutnamBench no-answer problems and DeepSeek-V3.1 seven (Section 5.2, p. 8). The paper also reports an average 23.7% seen-to-unseen drop and says the method’s net mean gain is 3.01% at pass@1 but slightly declines at pass@10 (Section 5.2, p. 9). A misplaced factorial in one generated statement passed Typecheck and the LLM Grader but failed BEq+ (Section 5.2, p. 8), illustrating that syntactic compilation and broad semantic judgment do not establish exact equivalence.

what is proved, trusted, and relevant to VL

The formal evidence consists of Lean compilation, rfl checks, BEq+ tactic attempts, and reported benchmark metrics. Trusted components include Lean 4.19.0-rc2, Mathlib imports, the gold formalisations, the LLM judge and back-translation model, and the assumption that benchmark rewordings preserve intent. Human annotation tunes ConJudge but does not prove every judge decision. Inference: the threat to agent-written verified Rust is high at the specification boundary: Verus can prove an incomplete ensures clause or a wrong conjecture. VL should treat conjecture generation and contract review as a separate measured stage and should not redo the basic seen-versus-unseen benchmark design. Existing work already demonstrates that examples and structured decomposition materially affect formalisation.

techniques for the catalog

• seen/unseen conjecture evaluation — separate translation with a supplied answer from autoformalisation that must infer the answer
• ConJudge completeness check — use a calibrated judge to test whether the generated statement contains the intended conjecture
• definitional conjecture metric — isolate candidate-answer generation with Lean rfl equivalence
• Lean-FIRe prompting — alternate natural-language decomposition with formal Lean translations, seeded by expert examples
• multi-metric validation — combine typechecking, tactic equivalence, and semantic judging to expose different failure modes Checked 2026-10-15 against paper sivakumar2025conjecturing: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15