Ce projet propose une bibliothèque Rocq qui automatise la traduction des bibliothèques HOL-Light vers Rocq, permettant d'utiliser des théorèmes et fonctions mathématiques dans Rocq. Il facilite l'interopérabilité entre ces deux systèmes de preuve formelle en alignant types et fonctions, et offre un accès à plus de 20 000 théorèmes couvrant des domaines variés comme l'arithmétique, l'algèbre, l'analyse ou la topologie. Les preuves traduites sont fournies sous forme d'axiomes pour une utilisation rapide, avec la possibilité de régénérer et vérifier les preuves originales si nécessaire.