Vérifier
Examiner les objets publics, leurs versions et exécuter les procédures de reproduction indépendantes.
Choisir d’abord un objet, puis sa version. Pour une reproduction publiée, partir du tag cité. Pour examiner les corrections documentaires ultérieures, utiliser le commit explicitement indiqué dans le dépôt.
Vérifications finies v1.0.0
git clone https://github.com/alexcour/couret-finite-verifications.git cd couret-finite-verifications git checkout v1.0.0 python -m pip install -r requirements.txt bash VERIFY_LOCAL.sh
Les sorties portent sur les calculs bornés inclus dans le paquet. Les évaluations flottantes et les prédictions conditionnelles conservent leur statut propre.
HOL-01 v1.1.1
git clone https://github.com/alexcour/hol01-monodromy-p7.git cd hol01-monodromy-p7 git checkout v1.1.1 python3 hol01_certificate.py --check RESULTS.json python3 independent_p7_permutation_check.py python3 finite_prime_regression_check.py --check FINITE_REGRESSION_RESULTS.json
Le certificat principal porte sur p=7. Les autres exécutions sont des contrôles finis supplémentaires ; elles ne démontrent pas un énoncé uniforme.
Traçabilité humain–IA v1.1.0
git clone https://github.com/alexcour/qui-repond-mathematiques-ia.git cd qui-repond-mathematiques-ia git checkout v1.1.0 python3 scripts/verify_release.py
La sortie attendue est « RELEASE VERIFICATION: OK ». Les 517 contrôles structurels, les quatre tests de mutation et les décomptes du corpus vérifient la cohérence du paquet ; ils ne valident pas les mathématiques rapportées.
Le tag publié précède l’ajout ultérieur des DOI sur main. Cette différence de métadonnées est documentée ; le tag demeure conservé.
Comment citer un contrôle
Indiquer le dépôt, le commit ou tag, la commande, l’environnement, la date et la sortie. Pour Lean, ajouter l’énoncé exact, les imports, la toolchain et les axiomes utilisés. Un badge vert ne remplace pas ces éléments.
Couret–Unification / InterIA · état documentaire au 1er octobre 2026. Une page scientifique ne doit jamais être plus affirmative que la pièce qui la soutient.
Portée de la vérification formelle
Lean contrôle un énoncé précis dans un environnement déterminé, avec les définitions, imports et axiomes réellement utilisés. Le statut de vérification formelle est attaché à cet énoncé et à une version accessible du code.
Chaque assertion de compilation doit renvoyer à son commit, à sa toolchain et à son journal d’exécution. Les décomptes de fichiers, de théorèmes et de sorry sont propres à un périmètre ; ils ne sont pas interchangeables. En l’absence de ces pièces, la compilation n’est pas présentée comme recontrôlée.
Cette vérification ne démontre ni la nouveauté, ni une interprétation globale absente de l’énoncé, ni la justesse d’une traduction mathématique qui n’aurait pas été auditée.
HOL2 et les réductions de congruence
Pour un premier impair p, la réduction SL₂(ℤ/pⁿ⁺¹ℤ) → SL₂(ℤ/pⁿℤ) ne se scinde pas lorsque n ≥ 2, ni lorsque n = 1 et p ≥ 5. Le cas n = 1, p = 3 est scindé. Il s’agit d’un phénomène classique ; le travail du programme porte sur sa présentation élémentaire, son rejeu exact et sa place dans le suivi des revendications.
Aucune nouveauté théorique générale n’est revendiquée. Cette note ne modifie pas le certificat HOL-01 p = 7 ni le corpus gelé v1.1.2. Référence : Stasinski, Journal of Algebra 566 (2021), §6.