Guide de Rethlas : comment exécuter Rethlas avec l'aide de l'IA (aucune connaissance en informatique requise)

Cette note propose un guide pas à pas pour utiliser Rethlas, un puissant système d'IA agentique dédié à la recherche mathématique autonome. Elle ne suppose aucune connaissance préalable en IA ni en informatique. Bien que ce ne soit peut-être pas la manière canonique d'utiliser Rethlas — un sujet que j'aborderai peut-être dans une note ultérieure — c'est sans doute la façon la plus simple de commencer.

Quelques remarques sur le public visé et le périmètre du guide :

• Aucune connaissance préalable en IA ou en informatique n'est requise. En particulier, vous n'avez besoin d'aucune expérience du terminal.
• Ce guide s'adresse aux utilisateurs de macOS et de Linux. Les utilisateurs de Windows peuvent le copier-coller dans un assistant IA et lui demander d'adapter les instructions pour Windows. J'utilise moi-même macOS et Arch Linux sur mes ordinateurs portables.
• Ce guide prend Codex CLI et les modèles Codex comme exemples, mais vous pouvez utiliser d'autres agents IA et d'autres modèles de base.
• Si le temps le permet, je prévois d'écrire d'autres guides sur des flux de travail agentiques utiles, sur la manière canonique d'utiliser Rethlas, et sur l'utilisation de Danus.

Qu'est-ce que Rethlas ?

En une phrase, pour les mathématiciens : Rethlas est un harnais qui rend l'IA nettement plus capable en recherche mathématique. Vous énoncez précisément une conjecture, et Rethlas travaille de façon autonome pour la prouver ou la réfuter — sans nécessiter d'autres instructions.

Pour plus de détails, voir l'article sur Rethlas [1].

D'après mes propres observations, Rethlas est nettement plus puissant que l'utilisation de l'IA via une simple interface de chat web. Par exemple :

Les expériences ont produit les comparaisons suivantes :

• Problème de groupes algébriques : Rethlas + GPT-5.5 xhigh > Rethlas + GPT-5.4 xhigh > GPT-5.5 Pro (voir [1, Section 5.1.1]).
• Problème de matroïdes : GPT-5.6 Sol max + Rethlas > GPT-5.6 Sol Ultra [2].

Rethlas a également résolu d'autres problèmes ; une sélection de résultats est présentée sur cette page GitHub.

Guide pas à pas (version paresseuse)

Étape 1 : Préparatifs

D'abord, ouvrez votre terminal.

Sur Mac, appuyez sur Command + Space pour ouvrir Spotlight, tapez Terminal, puis appuyez sur Enter.

Si vous ne l'avez jamais configuré, le terminal peut sembler laid ; ne vous laissez pas intimider.

Passons maintenant à l'étape la plus importante : installer une interface en ligne de commande (CLI) pour un agent IA.

Pour Codex, copiez-collez la commande suivante dans votre terminal, puis appuyez sur Enter :

curl -fsSL https://chatgpt.com/codex/install.sh | sh

Voir les instructions d'OpenAI pour Codex CLI. Pour Claude Code, voir les instructions d'installation d'Anthropic. D'autres CLI d'agents IA peuvent également convenir, mais ce guide utilise Codex de bout en bout.

Ensuite, créez un dossier nommé projects sur votre Bureau et placez-vous dedans. Sur Mac, copiez-collez les commandes suivantes dans votre terminal :

cd ~/Desktop
mkdir -p projects
cd projects

Lancez maintenant Codex CLI :

codex

Choisissez 1. Sign in with ChatGPT. Un abonnement ChatGPT Plus inclut l'accès à la famille de modèles GPT-5.6, y compris Sol ; les abonnements Pro offrent des limites d'utilisation plus élevées.

Une fenêtre de navigateur s'ouvrira. Connectez-vous à votre compte ChatGPT, puis revenez au terminal.

Une fois connecté et de retour dans le terminal, vous pouvez appuyer à tout moment sur Ctrl+C pour quitter Codex et revenir à l'invite de commande habituelle.

Vous êtes maintenant prêt à utiliser Codex CLI. Il fonctionne à peu près comme une interface de chat web, mais il peut accéder aux fichiers de votre dossier courant et — avec votre permission — exécuter des commandes dans le terminal. Ces capacités le rendent nettement plus puissant.

Vous pouvez poser des questions à Codex comme dans un chat web, mais relisez attentivement les commandes qu'il propose et assumez la responsabilité de tout ce que vous l'autorisez à exécuter.

Enfin, installons les paquets nécessaires :

Pour les utilisateurs de Mac :

brew update
brew install python
brew install git
brew install uv
brew install zola

Si vous voyez une erreur telle que command not found: brew, installez Homebrew en exécutant :

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

Suivez les instructions affichées par l'installateur de Homebrew, puis relancez les commandes d'installation ci-dessus. Si une autre erreur survient, copiez-collez le message complet dans Codex CLI et demandez-lui d'expliquer le problème et de vous aider à le corriger.

Sous Linux, installez ces paquets avec le gestionnaire de paquets de votre distribution. Par exemple, les utilisateurs d'Arch Linux peuvent utiliser sudo pacman -S au lieu de brew install.

Étape 2 : Configurer Rethlas

D'abord, clonez le dépôt Rethlas sur votre ordinateur :

git clone https://github.com/frenzymath/Rethlas rethlas

Placez-vous dans le dossier rethlas fraîchement téléchargé :

cd rethlas

Lancez maintenant Codex et demandez-lui de vous aider à configurer Rethlas. C'est délibérément l'approche la plus simple et la plus automatisée ; je compte expliquer la configuration manuelle canonique et le flux de travail correspondant dans un guide séparé.

Voici un exemple de prompt :

This repository contains an agentic framework for autonomous mathematical research. Please inspect the codebase carefully, using subagents in parallel where helpful. Identify and fix any issues that would prevent Rethlas from working on my laptop. In particular: (1) set up and use the correct virtual environments in `agents/generation/` and `agents/verification/`; `uv` is already installed; (2) ensure that `agents/generation/site/serve.sh` works on this laptop, adapting any hard-coded paths so that I can view the results through a local Zola server; and (3) identify and report any other bugs or setup issues.

Il n'est pas nécessaire de traiter tous les problèmes signalés par Codex ; les problèmes mineurs et bénins peuvent généralement être laissés tels quels. Vous pouvez utiliser GPT-5.6 Sol avec le raisonnement Extra High, voire GPT-5.5 avec le raisonnement Extra High. Ultra est superflu pour cette tâche de configuration simple. Pour Claude Code, Claude Opus 4.8 devrait suffire ; Claude Fable 5 est plus puissant que ne l'exige cette tâche.

Étape 3 : Laissez Rethlas résoudre votre problème

Vous pouvez demander à Codex CLI de lancer et de surveiller une expérience Rethlas pour vous.

Voici un exemple de prompt :

I want to use Rethlas to solve a research problem. Use GPT-5.6 Sol with Max reasoning as the base model for both the generation and verification agents. Ensure that the verification service is running and that both agents use the correct virtual environments. Then launch and monitor Rethlas as it attempts to solve the following problem: prove or disprove ...

Attendez maintenant de voir si Rethlas résout le problème. Vous pouvez de temps en temps demander à Codex où en sont les choses :

What is the current status?
Is the verification service healthy?
Has there been any recent progress?

Vous pouvez aussi fournir des indications mathématiques en fonction des progrès de Rethlas. Les utilisateurs de Claude Code peuvent utiliser /loop pour demander des vérifications d'état récurrentes tant que la session reste ouverte.

Étape 4 : Comment consulter le résultat

Si Rethlas produit une solution vérifiée, vous trouverez blueprint_verified.md dans agents/generation/results/. Si la vérification n'aboutit pas, vous y trouverez blueprint.md à la place ; ce brouillon n'a pas été accepté comme valide par l'agent de vérification.

Il y a deux façons de consulter le résultat :

Méthode 1 : Afficher le résultat dans un navigateur

Demandez à Codex CLI de servir le résultat localement :

Please use `agents/generation/site/serve.sh` to render the output blueprint at `http://localhost:3264`. Ensure that the MathJax syntax is correct, the document renders properly, and the MATbook theme is up to date.

Puis ouvrez un navigateur et rendez-vous sur http://localhost:3264.

Anecdote amusante/idiote : sur cette page, appuyez sur <shift>+f pour passer en plein écran, puis sur i pour entrer dans la Matrice.

Méthode 2 : Compiler le résultat en PDF avec LaTeX

Demandez à Codex CLI de convertir le fichier Markdown en LaTeX :

Convert the blueprint Markdown file into a compilable `amsart` LaTeX document. Do not alter the content. Ensure that all mathematical symbols render correctly and that all cross-references work.

Vous pouvez aussi demander à Codex de transformer le blueprint en brouillon d'article, mais vous ne devez pas supposer que le résultat est prêt à être publié.

Using `blueprint_verified.md`, write a professional, compilable `amsart` LaTeX manuscript suitable in style for a leading mathematics journal such as the *Annals of Mathematics* or *JAMS*. Present the mathematical content rigorously, coherently, and faithfully. Add an appropriate introduction and necessary citations, and avoid self-coined or unprofessional terminology. Do not alter the mathematical content of `blueprint_verified.md`.

Autres conseils

1. Rethlas, comme tout outil d'IA, n'est pas un oracle capable de résoudre tous les problèmes. Si Rethlas n'a pas résolu un problème après une longue exécution — disons 8 ou 24 heures — il vaut généralement mieux arrêter l'expérience. Vous pouvez alors essayer le système agentique plus puissant Danus [3] ; par exemple, Danus a résolu le problème de [4], alors que Rethlas n'y est pas parvenu. Sinon, il faudra peut-être découper le problème en sous-problèmes plus petits ou fournir des ingrédients non triviaux supplémentaires. Le problème peut aussi tout simplement dépasser les capacités des systèmes agentiques actuels — voire celles des modèles de base sous-jacents. Vous pouvez également essayer un modèle plus puissant, un effort de raisonnement plus élevé, ou les deux.

2. Lorsque vous fournissez des références au système, LaTeX ou Markdown est préférable au PDF. Vous pouvez utiliser un outil de reconnaissance optique de caractères (OCR) pour convertir un PDF dans l'un de ces formats.

3. Vérifiez soigneusement le résultat avant d'annoncer quoi que ce soit publiquement. Vous pouvez aussi essayer un outil d'autoformalisation. Je recommande Archon, un système agentique décrit dans [1] qui formalise les mathématiques de façon autonome en Lean 4. Attention toutefois aux pièges courants : les fichiers Lean peuvent contenir des sorry ou des axiomes supplémentaires, et les énoncés formalisés peuvent ne pas correspondre aux affirmations visées.

4. Si le processus est interrompu, pas de panique. Exécutez codex resume pour rouvrir la session Codex précédente, puis dites à Codex : Continue the experiment.

5. Transparence sur l'IA : même en l'absence de réglementation formelle, je pense que les chercheurs doivent être honnêtes et transparents sur leur usage de l'IA. Ma pratique consiste à expliquer dans les remerciements comment j'ai utilisé l'IA générative et, quand c'est possible, à donner plus de détails en annexe. Voir par exemple [2]. Si vous utilisez Rethlas, je vous serais reconnaissant de l'indiquer dans les remerciements. Voici un modèle suggéré :

The initial .... was discovered by Rethlas [1], an AI agent for mathematical research, developed by the Rethlas team, namely Haocheng Ju, Jiedong Jiang, Shurui Liu, Guoxiong Gao, Yuefeng Wang, Zeming Sun, Leheng Chen, Bin Wu, led by Professor Liang Xiao and Professor Bin Dong.

Pour une perspective communautaire plus large sur l'IA et les mathématiques, voir la Leiden Declaration on Artificial Intelligence and Mathematics [5].

Guides de suivi possibles

Si le temps le permet et si ces guides peuvent être utiles à la communauté mathématique, je pourrais écrire sur les sujets suivants :

1. Une manière plus directe et canonique de configurer et d'exécuter Rethlas sans déléguer le processus à une autre IA, y compris comment l'adapter pour prouver un lemme en utilisant les premières parties de votre article ;
2. D'autres flux de travail agentiques utiles, comme utiliser Codex pour améliorer la rédaction mathématique et corriger la grammaire, apprendre plus vite des domaines inconnus, ou organiser notes, aide-mémoire et polycopiés ;
3. Un guide d'utilisation de Danus ;
4. Une explication concise du code et de la méthodologie de Rethlas.

Références

[1] Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Liang Xiao, Ruochuan Liu, Bryan Dai, Bin Dong, et al. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789.

[2] Ronnie Cheng, Shurui Liu. Kazhdan-Lusztig polynomials of matroids need not be unimodal. arXiv:2607.24186.

[3] Jihao Liu, Guoxiong Gao, Zeming Sun, Bin Wu, Shurui Liu, Jiedong Jiang, Haocheng Ju, Leheng Chen, Ronnie Cheng, Xiping Zhang, Bin Dong. Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory. arXiv:2607.06447.

[4] Ronnie Cheng, Shurui Liu, Guoxiong Gao. Tangent classes of matroids and wonderful compactifications. arXiv:2607.05835.

[5] Leiden Declaration on Artificial Intelligence and Mathematics. Cette déclaration appelle à agir face aux défis posés par l'utilisation de l'intelligence artificielle dans la recherche mathématique. Elle est issue d'une initiative communautaire et est soutenue par l'Union mathématique internationale (IMU). Page web.