Benchmark · math

PutnamBench

2 résultats 1 modèles

PutnamBench est un benchmark de preuve formelle de théorèmes bâti sur des mathématiques de compétition universitaire : il mesure combien de problèmes de la compétition Putnam un système peut prouver au sein d'un assistant de preuve (Lean 4, Isabelle ou Coq), noté comme le nombre ou la proportion de preuves vérifiées par machine.

Exemple: Un problème difficile de Putnam de niveau universitaire — par exemple une affirmation de divisibilité en théorie des nombres, une borne d'une intégrale ou d'une inégalité, ou une identité combinatoire — présenté comme l'énoncé d'un théorème formel dont la preuve est laissée en `sorry` pour que le système la complète.
Notation: La métrique est le nombre (ou le pourcentage) de problèmes pour lesquels le système produit une preuve formelle complète. Un problème ne compte que si l'assistant de preuve le vérifie entièrement ; les arguments partiels ou le raisonnement informel valent zéro.
Vérification: Un résultat n'est accepté que lorsque le noyau de l'assistant de preuve cible type-vérifie toute la preuve sans `sorry`, sans axiome supplémentaire et sans modifier l'énoncé donné — le oui/non du vérificateur est le seul juge.
Pourquoi c'est important: Les problèmes de Putnam comptent parmi les mathématiques universitaires les plus difficiles, et les preuves vérifiées par machine ne laissent aucune place à un raisonnement incorrect ou « détourné », ce qui fait de PutnamBench un successeur rigoureux et bien plus ardu de MiniF2F pour la preuve automatique de théorèmes et le raisonnement mathématique.

Exemple résolu

Tâche

(Illustratif, simplifié.) Un théorème en Lean 4 au format PutnamBench, à prouver sans sorry : ```lean theorem putnam_illustrative (n : ℕ) : ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by sorry ```

Solution

```lean
theorem putnam_illustrative (n : ℕ) :
    ∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
  induction n with
  | zero => simp
  | succ k ih => rw [Finset.sum_range_succ, ih]; ring
```

Explication

La somme des n premiers nombres impairs vaut n^2 ; on le prouve par récurrence : le cas de base se ramène à 0 = 0, et l'étape utilise Finset.sum_range_succ, applique l'hypothèse de récurrence et clôt k^2 + (2k+1) = (k+1)^2 avec ring. Cela passe uniquement parce que le noyau de Lean accepte chaque étape — un vrai item de PutnamBench est bien plus difficile.

Leanstral 1.5

Chronologie

Date	Modèle	Score	Source
2026-07-03	Leanstral 1.5	587.0pts	Mistral a publié Leanstral-1.5-119B-A6B
2026-07-03	Leanstral 1.5	587.0pts	Leanstral 1.5 : Abondance de preuves pour tous