Shurui Liu

Rethlas-OSV : des agents mathématiques sur ordinateur pour les mathématiciens

Shurui Liu

J’ai récemment constaté que de nombreux mathématiciens souhaitent essayer des outils d’IA plus avancés qu’une interface de chat dans un navigateur, tels que les agents. Cependant, ils n’ont pas forcément le temps de se consacrer à l’ingénierie ou à l’informatique et ne souhaitent pas nécessairement travailler avec GitHub et le terminal.

J’ai donc décidé de créer des versions de bureau des agents mathématiques que j’ai contribué à développer. Ces applications sont conçues pour être faciles à installer et à utiliser au moyen d’une interface graphique, afin de faciliter la vie des mathématiciens.

Les programmes d’installation de la version bêta 0.5.1 de Rethlas-OSV sont disponibles ici :

Ces programmes d’installation nécessitent macOS 12 ou une version ultérieure.

Cette application de bureau a été développée en grande partie par « vibe coding » avec Claude Code Fable 5.1 et repose sur une première intégration d’OSVerify et de Rethlas réalisée par Fan Nie. Elle est actuellement en version bêta, et cette version ne propose des programmes d’installation que pour les utilisateurs de Codex sous macOS. Une prise en charge plus large pourra être ajoutée à l’avenir. Nous continuons également à améliorer OSVerify. N’hésitez pas à revenir consulter cette page pour obtenir les dernières mises à jour.

Qu’est-ce que Rethlas-OSV ?

Rethlas-OSV combine Rethlas et OSVerify et fonctionne avec Codex d’OpenAI. Il peut générer des preuves et signaler d’éventuelles imprécisions dans un article mathématique donné.

Rethlas est un cadre agentique de raisonnement mathématique automatisé, développé par Haocheng Ju, Jiedong Jiang, Shurui Liu, Guoxiong Gao, Yuefeng Wang, Zeming Sun, Leheng Chen et Bin Wu, sous la direction des professeurs Liang Xiao et Bin Dong. Rethlas est entièrement open source sur GitHub. Son rapport technique présente également Archon, un cadre agentique d’autoformalisation en Lean 4.

OSVerify est un cadre agentique de vérification, développé par Fan Nie, Haotian Ye, Shurui Liu, Zihao Wang, Stefano Ermon et James Zou. L’article et le code d’OSVerify seront bientôt publiés.

Pourquoi est-ce que je pense qu’il est plus puissant que le modèle de base utilisé seul ?

Il n’existe aucune preuve théorique ni aucune garantie que ce dispositif améliore les capacités du modèle de base, mais de nombreuses études de cas semblent l’indiquer. Certaines figurent dans le rapport technique de Rethlas et dans le prochain article consacré à OSVerify. Plusieurs utilisateurs ont également constaté des améliorations par rapport à l’utilisation du seul modèle de base avec GPT-5.5 Pro, GPT-5.6 Sol et GPT-6-Astra.

Comment l’utiliser

Installation

  1. Téléchargez l’application adaptée à votre Mac : Apple silicon (arm64) ou Intel (x86_64). Pour identifier votre processeur, ouvrez le menu Apple dans le coin supérieur gauche de l’écran et sélectionnez About This Mac.
  2. Double-cliquez sur l’image disque et faites glisser Rethlas-OSV dans Applications. Si macOS vous propose de placer l’application dans la corbeille, ne sélectionnez pas Move to Trash.
  3. Lors du premier lancement, vous devez autoriser l’ouverture de l’application. Double-cliquez une première fois sur celle-ci et fermez l’avertissement en sélectionnant Done. Ouvrez ensuite System Settings, sélectionnez Privacy & Security, faites défiler la page vers le bas et cliquez sur Open Anyway à côté du message concernant Rethlas-OSV.

Vous pourrez ensuite l’utiliser comme n’importe quelle autre application sur votre MacBook. Appuyez sur command+space et saisissez reth pour l’ouvrir rapidement.

Se connecter à votre compte Codex

Ouvrez Settings et cliquez sur Sign in.... Rethlas-OSV ouvrira votre navigateur et vous demandera de vous connecter au compte OpenAI que vous utilisez avec Codex.

Paramètres de connexion à Codex CLI dans Rethlas-OSV

Repérer les erreurs dans un article

Vous pouvez utiliser Rethlas-OSV pour repérer les erreurs dans un article. Chargez le code source LaTeX ou le fichier Markdown de l’article, puis donnez un nom à l’exécution.

Chargement d’un article et choix d’un mode de vérification dans Rethlas-OSV

Choisissez ensuite un mode. Dans le mode Smart, sélectionné par défaut, l’agent choisit les théorèmes principaux ainsi que les étapes clés dont ils dépendent.

Options de vérification et bouton Start review dans Rethlas-OSV

Décidez ensuite si vous souhaitez activer Stop on audited rejection. Lorsque cette option est activée, l’évaluation s’arrête de manière anticipée si elle aboutit à une décision auditée REJECT. Lorsqu’elle est désactivée, l’agent mène l’ensemble du processus à son terme et signale tous les problèmes qu’il a trouvés.

Après avoir choisi le modèle et l’effort de raisonnement, cliquez sur Start review.

Prouver une conjecture ou un lemme

Donnez un nom à cette exécution. Vous pouvez ensuite saisir le problème, par exemple :

  • Prove Conjecture 4.16 in arXiv:xxxx.xxxx.
  • Prove or disprove the conjecture that ...
  • Chargez le fichier LaTeX de votre travail en cours et ajoutez Prove the lemma {LaTeX tag} in the following paper au début.
Configuration d’une exécution de génération de preuve dans Rethlas-OSV

Choisissez ensuite le modèle, l’effort de raisonnement, le nombre maximal de tours par branche (le nombre d’itérations qui seront tentées) et le nombre de branches parallèles (le nombre d’agents de génération qui doivent travailler en parallèle sur différentes stratégies).

Cliquez sur Start proving pour commencer.

Gérer les exécutions

Vous pouvez annuler une exécution et la reprendre plus tard. Si vous avez épuisé votre quota GPT ou devez éteindre votre ordinateur portable, ne vous inquiétez pas : le travail déjà accompli est conservé et vous pourrez reprendre l’exécution ultérieurement.

Conseils aux utilisateurs

  1. Rethlas-OSV nécessite un abonnement GPT. Ses paramètres, ainsi que les données saisies, les rapports et les enregistrements associés à chaque exécution, restent sur votre ordinateur ; l’application de bureau les stocke dans ~/Library/Application Support/Rethlas-OSV/. Les appels aux modèles sont envoyés à OpenAI par l’intermédiaire de Codex CLI avec votre propre compte. Rethlas-OSV ne stocke aucune donnée d’authentification ; en dehors des appels aux modèles adressés à OpenAI par l’intermédiaire de Codex, il n’envoie aucune donnée ailleurs.
  2. Veuillez utiliser Rethlas-OSV de manière responsable. Les points de vue philosophiques sur l’avenir des mathématiques et de leurs protocoles peuvent varier, mais assurez-vous au moins que votre intention est de contribuer au bien de la communauté mathématique et de l’humanité.
  3. Surveillez votre consommation sur votre compte GPT. Un flux de travail agentique peut être coûteux, car il appelle continuellement le modèle de base.
  4. Si vous utilisez Rethlas-OSV pour générer des preuves, veillez à créditer correctement les contributions de chacun. Il se peut qu’une solution générée ne cite pas convenablement les travaux antérieurs ou les travaux en cours dans la communauté mathématique.
  5. Si vous utilisez Rethlas-OSV pour évaluer des articles, veillez à obtenir l’autorisation des auteurs, de la revue et de toute autre partie concernée. Rethlas-OSV signale uniquement les problèmes de validité détectés et ne porte aucun jugement sur la nouveauté ou l’importance d’un article.
  6. Comme tout outil d’IA en mathématiques, Rethlas-OSV ne garantit pas l’exactitude de ses résultats.
  7. Faites preuve de transparence quant à votre utilisation de l’IA générative. Faites appel au bon sens et à votre propre jugement.
  8. Nous vous serions très reconnaissants de citer nos articles.

Références

[1] Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai et Bin Dong. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789, 2026.

[2] Fan Nie, Haotian Ye, Shurui Liu, Zihao Wang, Stefano Ermon et James Zou. One-Sided Verification Under Limited Expert Review. Article soumis, 2026.

BibTeX

@misc{rethlas_archon2026,
  title  = {Automated Conjecture Resolution with Formal Verification},
  author = {Haocheng Ju and Guoxiong Gao and Jiedong Jiang and Bin Wu and
            Zeming Sun and Shurui Liu and Leheng Chen and Yutong Wang and
            Yuefeng Wang and Zichen Wang and Wanyi He and Peihao Wu and
            Liang Xiao and Ruochuan Liu and Bryan Dai and Bin Dong},
  note   = {arXiv:2604.03789},
  year   = {2026},
}

@misc{osv2026,
  title  = {One-Sided Verification Under Limited Expert Review},
  author = {Fan Nie and Haotian Ye and Shurui Liu and Zihao Wang and
            Stefano Ermon and James Zou},
  note   = {In submission},
  year   = {2026},
}

Une démonstration plus détaillée

Une démonstration plus détaillée sera ajoutée ici.

Remerciements

Je remercie sincèrement toutes les personnes avec lesquelles j’ai collaboré dans le cadre de Rethlas et d’OSVerify. Je tiens tout particulièrement à remercier Bin Dong, Guoxiong Gao, Haocheng Ju, Fan Nie et Haotian Ye pour leur soutien et pour la formidable expérience que représente notre collaboration.

Je tiens également à remercier les membres de la communauté mathématique de Stanford pour leur soutien constant. Je remercie tout particulièrement Kevin Rizk et Henry Bosch d’avoir testé l’application de bureau avant que je ne la rende publique.

Comments