Ce projet propose une traduction de la bibliothèque arithmétique de Matita vers le langage Agda. Il facilite l'échange et la vérification de preuves mathématiques entre différents systèmes formels. L'objectif est d'améliorer l'interopérabilité et la réutilisation des travaux en logique et en mathématiques formelles.