Title: A Formal Approach to Resolving Answer-Construction Challenges in Lean

Abstract: Mathematical competition tasks generally categorize into two distinct categories: theorem proving, which demands a rigorous proof for a specified proposition, and answer construction, which necessitates the creation of an object that satisfies specific properties, accompanied by supporting proofs. While large language models (LLMs) have driven significant improvements in formal theorem proving for the former, the latter area remains comparatively underexplored. This disparity highlights a critical gap between existing LLM architectures. General-purpose LLMs excel at informal conjecture generation but suffer from high costs and unreliability when generating formal proofs. Conversely, prover-optimized LLMs are cost-effective and tailored for formal verification but lack the mathematical reasoning capabilities required to propose viable candidate answers. Furthermore, standard Lean proof checking fails to guarantee that a constructed witness represents a canonical solution; circular references or non-closed-form witnesses may successfully discharge existential quantifiers yet remain inadmissible as contest responses. To bridge this divide, we present Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework within Lean designed for end-to-end answer construction with formal verification. ECP utilizes tool-assisted general LLMs to survey evidence and generate candidate solutions, subsequently employing prover LLMs to generate machine-verifiable proofs. In evaluations on PutnamBench and the autoformalized MathArena, ECP successfully produced admissible answers and proofs for 17 out of 346 instances on PutnamBench and 18 out of 75 on MathArena, surpassing LLM baselines within comparable inference budgets. The implementation is accessible at https://github.com/sunjia72/ecp-lpar.

Source: arXiv Generated at: 2026-06-02 00:00:00 UTC