[Veille→Distillation] open-ontologies (Rovai) — proof-carrying inference pour le Web Sémantique : le pont SW-13 ↔ vericode #16751 — certificats d'inférence vérifiés Lean (SHIQ/Horn/SWRL) #16855

Origine

Demande Emerjesse (19/09, Telegram) : considérer l'intégration/distillation de fabio-rovai/open-ontologies — « SW + Lean résonne pas mal, et fait le complément de vericode de l'Epic Tegmark ».

Verdict : résonance réelle et précise — c'est le pont manquant entre notre série SemanticWeb et la vague vericoding (#16751). Le dépôt est aussi une leçon d'ingénierie logicielle rare (honnêteté documentaire exemplaire), ce qui en fait un cas d'étude en soi.

Le dépôt (lu firsthand — README complet, historique commits, arborescence)

Open Ontologies : plateforme d'ingénierie et de vérification d'ontologies et graphes de connaissances — Rust 58,8 %, Lean 11,7 %, Python 13,4 %, Isabelle 2,5 %, TypeScript (studio web). MIT. 514 stars, 69 forks, 7 contributeurs. Actif : dernier commit il y a 3h, v1.4.0 le 15/09, 788 commits depuis mars 2026. 2 préprints arXiv associés : Open Ontologies (2605.09184) et CIVeX (2605.09168, causal intervention verification).

Le concept central : proof-carrying inference. Chaque conclusion du raisonneur (RDF/OWL SHIQ, Horn/SWRL/RIF) s'accompagne d'un certificat qu'un checker séparé, écrit en Lean 4 et prouvé sound, accepte ou rejette. La table « With a proof, and without one » du README est un cours entier : « Ask a reasoner why it believes something and it will tell you to trust it. This one hands you a proof, and refuses a forged one. »

Architecture multi-vérificateurs (rare, pédagogiquement précieuse) :

• Lean 4 (lean/OOCert) : soundness du certificate checker Horn — horn_certificate_sound
• Isabelle + Rocq : formalisations indépendantes du même checker (le commit feat(SC-5): convert print-only cells to executable compile_and_deploy #186 documente une divergence réelle trouvée par le différentiel : Lean saute une ligne vide, Rocq refuse — 1 divergence/1 593 lignes, cause unique)
• Aeneas : traduction Rust→Lean du boundary core (14 théorèmes non bornés)
• Dafny : l'interner prouvé (injectivité, round-trip) — avec justification mesurée du déclassement de Kani
• Z3 + cvc5 en oracles différentiels ; E/Vampire/Mace4 pour le FO

L'honnêteté documentaire comme discipline de code (les commits sont un cours) :

• commit 55abe97 : « Correct the claims the docs made about the engine » — sweep de 10 claims, 131 corrections sur 37 fichiers : « 109 tools, not 70+, 50+, 103 or 43 as four files variously said » ; « the reasoner is SHIQ, not SHOIQ » ; « 0 disagreements with HermiT » corrigé en « 0 unsound rejections » (23/78 884 paires au tier résiduel)
• Décision 0006 : unat = opinion d'oracle, jamais habillée du vocabulaire du checker
• Le studio colore les arêtes par warrant (asserted/derived-checked/refused) et refuse délibérément une catégorie « unproved » non mesurée
• tests qui vérifient que les counts des docs sont dérivés, pas typés à la main (no_stale_tool_count_survives_anywhere)

Résonances dans CoursIA — vérifiées firsthand

1. ⭐ La série SemanticWeb complète, au concept près

SymbolicAI/SemanticWeb/ : SW-1→15 (RDF, SPARQL, RDFS, OWL, SHACL, KnowledgeGraphs, GraphRAG, Reasoners, Coup Ontologique, Coup Argumentatif). SW-13-Python-Reasoners (93 cellules) compare owlrl/HermiT/reasonable/Growl — HermiT cité 95×, mais certificate : 0 hit, proof : 0, justif : 0. Le concept de preuve transportable est exactement le gap.

2. ⭐⭐ Le complément vericode de l'Epic Tegmark #16741

Emerjesse l'a nommé : c'est le complément de #16751 (vericoding vs vibe coding). Le lien est structurel :

• Vericoding vs vibe coding : preuve formelle de programmes générés par LLM #16751 : prouver les programmes générés par LLM (Aeneas, Dafny, Lean) ;
• open-ontologies : prouver les inférences d'une base de connaissances — la même chaîne vérification formelle appliquée au Knowledge Graph.

Notre série SW s'arrête à « le raisonneur a dit » ; l'Epic Tegmark/vericode veut « la preuve en main ». Open-ontologies est l'implémentation de référence de ce pont : un LLM (Claude, via MCP) écrit l'ontologie, le moteur certifie, Lean prouve le certificat. La boucle « agent écrit → machine prouve » de #16751, incarnée dans le Web Sémantique.

3. Ponts additionnels vérifiés

• SMT/Z3 : SymbolicAI/SMT/Z3-Linq2Z3/ (10 notebooks) — le dépôt utilise Z3 comme oracle différentiel ; nos notebooks SMT sont le prérequis naturel.
• Tweety/Argumentation : SW-15-Python-Coup-Argumentatif + argumentation_lean — les justifications minimales (Reiter hitting-set, onto_justify) résonnent avec l'argumentation formelle.
• Claude Code plugin + MCP : le dépôt shipe un plugin Claude/ClawHub — même pattern que nos lanes (l'IA générative qui écrit, le checker qui prouve).
• CIVeX (2605.09168) du même auteur : causal intervention verification pour agents — à garder en veille séparée (un autre mandat potentiel).

Ce qui est distillable (honnêteté Mimo)

Oui :

• le concept proof-carrying inference : certificat = fichier vérifiable par un tiers qui ne fait pas confiance au moteur — implémenter une version jouet (Horn + quelques règles OWL, checker séparé en Python, forge d'un certificat → rejet) ;
• la table « with a proof / without one » comme fil rouge pédagogique ;
• le pattern multi-vérificateurs différentiels (Lean + Isabelle + Rocq + Dafny sur le même objet) ;
• l'anti-leçon « unsat est une opinion d'oracle » ;
• le cas d'étude honnêteté documentaire (commit 55abe97) pour la culture « claims mesurés, pas tapés » — écho direct de notre règle sota-not-workaround.md.

Non / à assumer :

• le moteur Rust complet (109 outils MCP) n'est pas à porter — le binaire est utilisable tel quel ;
• les preuves Lean/Isabelle/Rocq existantes sont citées, pas reprises ;
• dépôt jeune (6 mois) et majoritairement co-écrit avec Claude (commits co-signés) — qualité de discipline documentaire remarquable, mais stabilité API non garantie ; figer un tag pour toute utilisation.

Options

A. (recommandée) Grain SW-16 « Proof-Carrying Ontologies » — le certificat d'inférence, jouet complet : ontology Horn jouet + moteur de dérivation Python naïf + émission de certificats + checker indépendant (accepte/rejette, forge = rejet nommé) ; comparaison avec le vrai binaire open-ontologies (install ou Docker) sur la même ontologie jouet ; la table « with/without proof » en fil rouge ; cross-links SW-13 (le gap), #16751/#16741 (le pont vericode), Z3-Linq2Z3 (oracles différentiels), Tweety (justifications). Encart « l'honnêteté documentaire comme discipline » (commit 55abe97 comme cas d'étude).

B. Intégration-outil : adoption du binaire dans la série SW existante (SW-13 bis « un raisonneur qui prouve ») sans nouveau grain — plus léger, mais laisse le concept non formalisé.

C. Les deux séquencés : A d'abord (le concept), B ensuite (l'outil) quand le grain existe.

D. Veille seule — insuffisant : le gap SW-13 est précis (0 certificat/preuve) et le pont vericode désigné par Emerjesse.

Précautions

• Dédup vérifié : aucune issue existante (open-ontologies / rovai / 2605.09184 → 0 hit pertinent, 19/09).
• Figér le tag pour toute utilisation du binaire (v1.4.0 le plus récent ; l'historique montre des corrections de claims post-release).
• Ne pas canoniser les chiffres du README (514 stars etc. seront périmés) : les nombres de tests/outils évoluent vite — citer tag+date.
• CIVeX = mandat séparé potentiel (ne pas fusionner).
• Le dépôt a un plugin Claude Code : si adoption, vérifier la politique de dépendances du dépôt CoursIA pour les outils externes.

Traçabilité protocole

• Claim : [CLAIM-VEILLE] github.com/fabio-rovai/open-ontologies — Hermes — 17/09 posté avant analyse ✓
• Check avant create : 0 doublon ✓
• Rôle NanoClaw : reviewer attendu (angle mort check).

Issue ouverte par Hermes (myia-po-2026) sur demande Emerjesse, 19/09/2026. Dépôt lu firsthand (README 618 lignes cache local, historique commits, languages, releases). Résonances vérifiées : arbre SW-1→15, SW-13 grep (certificate/proof/justif : 0), #16751/#16741, Z3-Linq2Z3, argumentation_lean. Dédup 0.