Language models, meet formal mathematics

Can language models prove it?

Real theorems from Mathlib. Proofs written by AI. Checked by Lean.

Problems solved

Compiler acceptance · up to 3 attempts

GPT-5.4OpenAI

53.6%

Mathlib problems: 1,513
Accepted solutions: 811
Attempts per problem: ≤ 3

An exploratory run, including potential theorem reuse.
Read the methodology

A closer look

One theorem. Two ways through.

Accepted on attempt 2

If a prime divides a finite product, it divides at least one of its factors. Mathlib reuses a result about multisets; GPT-5.4 proves it by induction on the finite set.

Mathlib

Reference proof

import Mathlib

variable {ι M M₀ : Type*}
variable [CommMonoidWithZero M₀] {p : M₀}

theorem exists_mem_finset_dvd
    (hp : Prime p) {s : Finset ι} {f : ι → M₀} :
    p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=
  Prime.exists_mem_multiset_map_dvd hp

Reuse the corresponding multiset theorem.

GPT-5.4

Generated proof

import Mathlib

variable {ι M M₀ : Type*}
variable [CommMonoidWithZero M₀] {p : M₀}

theorem exists_mem_finset_dvd
    (hp : Prime p) {s : Finset ι} {f : ι → M₀} :
    p ∣ s.prod f → ∃ i ∈ s, p ∣ f i := by
  classical
  refine Finset.induction_on s ?_ ?_
  · intro h
    exfalso
    exact hp.not_dvd_one h
  · intro a s ha ih hdiv
    rw [Finset.prod_insert ha] at hdiv
    rcases hp.dvd_or_dvd hdiv with hpa | hps
    · exact ⟨a, Finset.mem_insert_self a s, hpa⟩
    · rcases ih hps with ⟨i, his, hpi⟩
      exact ⟨i, Finset.mem_insert_of_mem his, hpi⟩

Build an induction proof, without calling the target theorem.

From the cached benchmark run. Shared context is preserved; line breaks are adjusted for display.

View the full attempt

Beyond the score

From a working proof to a better one.

Leaner is a small experiment in formal reasoning: measure what a model can prove, compare its work with Mathlib, and turn those differences into data for learning.

Explore the fine-tuning dataset How it works