Séminaire Cambium, Inria Paris
                                 Amphi Lions
                         Vendredi 5 septembre, 10h30

                                 Huajian Xin
                           University of Edinburgh

    Formal Mathematics at Scale: From Theorem Proving to Proof Engineering

Recent advances in AI-assisted theorem proving have greatly expanded
the scope of formal mathematics. This talk presents Seed-Prover, a
state-of-the-art system for Lean 4 that combines AI with interactive
theorem provers to solve challenging problems. Seed-Prover follows a
lemma-centric design, decomposing complex proofs into atomic steps for
long-horizon reasoning. Its multi-stage workflow integrates conjecture
generation, verifier-guided training, and scalable inference modes
(Light, Medium, Heavy) tailored to problem difficulty. This approach
has set new benchmarks on miniF2F and Putnam Bench, and achieved a
silver-medal level performance at the 2025 International Mathematical
Olympiad.

The second part of the talk shifts focus from static benchmarks to the
ongoing challenge of proof engineering: maintaining and extending
large formal libraries such as Mathlib. Existing benchmarks overlook
this dynamic, engineering-heavy process. To address this gap, we
introduce APE-Bench I, a benchmark that frames the task as applying
natural-language instructions to a live formal codebase. APE-Bench I
uses two layers of evaluation: syntactic validation via the Lean
compiler and semantic assessment via an LLM judge. Early results show
that even top models falter on this more realistic setting,
underscoring the need for new methods.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.