Nous présentons un agent d'apprentissage in-context pour la démonstration formelle de théorèmes dans des environnements tels que Lean et Coq. Les modèles actuellement les plus performants pour ce problème sont entraînés sur des données de preuves spécifiques à chaque environnement. À l'inverse, notre approche, appelée COPRA, sollicite répétitivement un modèle de langage massif à haute capacité et généraliste (GPT-4) afin qu'il propose des applications de tactiques au sein d'une recherche arrière (backtracking) étatique. Les tactiques proposées sont exécutées dans l'environnement de preuve sous-jacent. Les retours générés par l'exécution sont utilisés pour construire le prompt de la requête suivante, en combinant des informations sélectionnées de l'historique de recherche et des lemmes récupérés depuis une base de données externe. Nous évaluons notre implémentation de COPRA sur le benchmark miniF2F pour Lean ainsi que sur un ensemble de tâches Coq issues du projet CompCert. Sur ces benchmarks, COPRA surpasse significativement les appels peu nombreux (few-shot) de GPT-4. Elle se compare également favorablement aux approches basées sur l'entraînement sur mesure, dépassant ReProver, une approche entraînée sur mesure d'état de l'art pour Lean, en termes de métrique pass@1. Notre code et nos données sont disponibles à l'adresse suivante : https://github.com/trishullab/copra.