Les grands modèles linguistiques ont récemment fait des progrès significatifs dans la génération de preuves mathématiques rigoureuses. En revanche, leur utilisation pour la démonstration de théorèmes dans des langages formels (tels que Lean) reste difficile et coûteuse en ressources computationnelles, en particulier pour des problèmes au niveau du baccalauréat et au-delà. Dans ce travail, nous présentons Seed-Prover 1.5, un modèle de démonstration théorème formel entraîné par apprentissage par renforcement agencé à grande échelle, accompagné d’un flux de travail d’échelle au moment du test (test-time scaling, TTS) efficace. Grâce à des interactions étendues avec Lean et d’autres outils, le modèle accumule continuellement de l’expérience durant le processus d’apprentissage par renforcement, ce qui améliore considérablement sa capacité et son efficacité en matière de démonstration formelle. Par ailleurs, en tirant parti des avancées récentes dans les preuves en langage naturel, notre workflow TTS permet de combler efficacement le fossé entre les langages naturels et les langages formels. Par rapport aux méthodes de pointe, Seed-Prover 1.5 atteint des performances supérieures avec un budget informatique réduit. Il résout 88 % des problèmes de PutnamBench (niveau licence), 80 % de Fate-H (niveau master) et 33 % de Fate-X (niveau doctorat). Notamment, en utilisant notre système, nous avons résolu 11 des 12 problèmes du Putnam 2025 en moins de 9 heures. Nos résultats suggèrent que l’augmentation de l’apprentissage à partir de l’expérience, alimentée par un retour formel de haute qualité, recèle un potentiel considérable pour l’avenir du raisonnement mathématique formel.