Trois types de résultats, trois portées.
Expériences numériques
Les tests mesurent des comportements sur des fonctions, des départs et des budgets précis. Ils ne démontrent pas la convergence sur tout problème possédant une racine.
Preuves mathématiques
Les énoncés Lean portent sur des identités exactes et des bornes conditionnelles. Ils ne vérifient pas de bout en bout Python, NumPy ou l’évaluation d’un callback.
Campagne 449 contre 448
Chaque configuration emploie le même callback et le même départ, sans Jacobien analytique fourni, avec au plus 6 000 évaluations physiques. Trois répétitions intercalées sont réalisées ; une réussite stable exige trois verdicts positifs.
| Ensemble | Configurations | 448 | 449 |
|---|---|---|---|
| Ensemble connu | 14 695 | 14 673 réussites | 14 675 réussites |
| Graines réservées | 3 300 | 3 295 réussites | 3 295 réussites |
| Total | 17 995 | 17 968 réussites | 17 970 réussites |
Aucune configuration réussie par 448 n’est perdue par 449 dans cette campagne. Le total comprend 25 configurations encore en échec. Les configurations connues incluent des cas de développement, des tests historiques, des exemples structurels et des diagnostics ciblés ; ce n’est pas un échantillon entièrement indépendant.
Les racines exigent un résidu euclidien au plus égal à 10−8. Les modes de moindres carrés et certains problèmes MGH conservent leurs juges historiques, qui peuvent accepter un objectif positif. Une réussite n’y signifie donc pas nécessairement une racine.
Les temps sont les sommes des médianes par configuration, hors préparation et juges : 46,600 s contre 46,602 s sur l’ensemble connu, et 7,950 s contre 7,928 s sur le lot réservé (449 contre 448). Ils dépendent de la machine et du coût des fonctions.
Portée du bundle Lean 449
Le bundle compte 100 énoncés uniques, dont deux nouveaux résultats sur la réserve du budget de sondes. Il a été vérifié avec Lean 4.33.1 et Mathlib v4.33.1 dans Docker, sans sorry, admit, axiome personnalisé ou oracle numérique.
- Monotonie de la politique de quota avec la précision du candidat.
- Conservation d’une capacité réservée sous des hypothèses de comptes exacts.
- Identités et bornes mathématiques conditionnelles héritées des versions précédentes.
Le diagnostic |J|·ulp reste une heuristique linéarisée. Les certificats résiduels exacts concernent les valeurs binary64 retournées, pas l’erreur complète d’une fonction mathématique idéale. Aucun théorème de convergence universelle à budget fini n’est annoncé.