Large Language Models for Mathematical Discovery: Generation, Verification, and Knowledge Provenance

Formal mathematics has a data problem, and large language models have become one of the tools applied to it. LeanConjecturer mined 40 seed files from Mathlib and produced 12,289 candidate statements, of which 3,776 resisted the automated tactic used as a filter. AlphaGeometry solved 25 of 30 olympiad geometry problems by letting a language model propose auxiliary constructions whenever symbolic deduction stalled. FunSearch improved on earlier results for the cap set problem by having an evaluator score programs written by a model. Evidence of this kind still supports a narrower claim than mathematical discovery. Five studies are compared in this review: LeanConjecturer, the Conjecturing-Proving Loop, AlphaGeometry, FunSearch, and Unlearning as Ablation. Using literature analysis and comparative case analysis, task objectives, generation mechanisms, verification procedures, and evidential limits are examined side by side. Two findings stand out. External verification is what makes candidate selection and iterative repair function in each system, and each system demonstrates a different slice of the work: conjecture supply, proof repair, geometric construction, program optimization, and, in the case of Unlearning as Ablation, a proposal for auditing knowledge provenance. Correctness, novelty, and independence from previously acquired target knowledge remain three separate questions that require three separate kinds of evidence. A more reliable evaluation framework would combine auditable knowledge boundaries, dependency checking, and expert assessment of mathematical significance.