Repository navigation
feat(leandojo,#18562 pli 2): integration leandojo dans prouveur maison -- evaluation faisabilite #18915
Description
Activity
[CLAIMED] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/Lean/agent_tests/prover/integration/**
Grain: DEEP/notebook-python -- lane myia-ai-01:CoursIA-2 -- prev: MED/guard #18896
Sous-grain du EPIC #18430 (intégration LeanDojo-v2). Scope cycle c.76 : (1) vérifier que lean-dojo v2.2.0 (deja epingle dans Lean-10) est invocable model-only sans GPU ni dataset de competition ; (2) tester l'API model sur un mini-theoreme Lean-10 deja prouve ; (3) poser un verdict SOTA (SOTA-OK / RECOVERABLE-LOCAL / INTRINSIC) documente. Pas de GPU requis (lean-dojo model-only CPU). Issue de suivi fille de #18430, followup de #18893.
Tell c.1502 strict fondateur
[CLAIMED-AMEND] lane myia-ai-01:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/**, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-10-LeanDojo.ipynb
Grain: DEEP/notebook-python -- lane myia-ai-01:CoursIA-2 -- prev: MED/guard #18896
Amendement de mon claim precedent (comment 5963859492) : le bon chemin est SymbolicAI/Lean/agent_tests/prover/integration/, pas Lean/agent_tests/prover/integration/. Le sous-dossier SymbolicAI/Lean contient deja Lean-10 (LeanDojo v1) et le repertoire agent_tests/prover qui sera amene a integrer LeanDojo v2. Scope cycle c.76 inchange.
Tell c.1502 strict fondateur
Verdict SOTA etude de faisabilite LeanDojo v2 --
[myia-ai-01:CoursIA-2]-- 2026-10-03T04:05ZPer claim-AMEND 5963862545 (pli 2 #18562 via #18893). Mesure firsthand sur Python 3.10.11 (kernel jupyter python3 -- C:\Users\PYIA\AppData\Local\Programs\Python\Python310\thon.exe).
5 axes testes
# Axe Verdict Mesure 1 Compatibilite Python + lean-dojo RECOVERABLE-LOCAL Python 3.10.11 + lean-dojo 4.20.0, pip install lean-dojoOK (~10 s, sans torch/transformers)2 Modules sans torch RECOVERABLE-LOCAL Subset LeanGrepo,trace,is_available_in_cache,Dojo,Theorem,check_proof, ... importable3 LeanGrepo + is_available_in_cache RECOVERABLE-LOCAL Signature 4.20.0 = is_available_in_cache(repo: LeanGrepo)(signature changee depuis la doc c.76)4 Trace repo Lean 4 RECOVERABLE-LOCAL (conditionnel) Necessite Lean 4 toolchain local ( lean --version) + reseau GitHub valide + cache pre-rempli5 Model ML LeanDojo (torch/transformers) INTRINSIC torch + transformers non dispos localement (~2 GB), GPU preferable pour inference ; semantique INTRINSIC (axe 5 N/A parce que la cible requiert un runtime ML non testable ici) Conditions RECOVERABLE-LOCAL
- Python 3.10-3.12 (lean-dojo 4.20.0 Requires-Python >=3.9,<=3.12). Python 3.14 NON compatible.
- Lean 4 toolchain local (
lean --versiondoit fonctionner, ex. viaelan) - Reseau HTTPS valide (GitHub.com accessible pour
LeanGrepoctor et cache pre-rempli) - Certificats SSL a jour dans l'env Python (sinon SSL verify fail sur ctor ; verifie
https://github.com= 200 depuis l'env)
Hors scope (mesure)
- torch / CUDA : axe 5 = INTRINSIC. Si on veut le model ML, router vers une lane GPU (po-2024).
- Dataset de competition LeanDojo (BountyBench, miniF2F) : hors scope pli 2 (focus model only).
Recommandation pour pli 2
Implementer un carnet
Lean-11-LeanDojo-V2-Faisabilite.ipynbfocalise sur les axes 1-4 (tracage repo Lean 4 simple, sans torch) une fois les conditions RECOVERABLE-LOCAL verifiees (Lean 4 toolchain + reseau).Le model ML reste en INTRINSIC tant qu une lane GPU n est pas mobilisee.
Preuve d execution
Notebook execute dans scratchpad (
C:\Users\MYIA\AppData\Local\Temp\LeandojoV2_NB_executed.ipynb, 4/4 cells, outputs ci-dessus) ; pas commitee dans le depot (sort de scope c.78 : DEEP/lean exige un carnet execute avec Lean 4 toolchain locale).Refs: PR #18893 (pli 1 stubs), issue #18915 (pli 2 faisabilite), issue #18562 (pli mere).
Grain: DEEP/notebook-lean -- lane myia-ai-01:CoursIA-2
- added 5 commits that reference this issue
on Oct 3, 2026 - added a commit that references this issue
on Oct 3, 2026 [CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-2
issue: 18915
verdict: CLOSE
acceptance:- verdict SOTA etude faisabilite LeanDojo v2 -> PR feat(leandojo,#18915 pli 2): integration leandojo v2 dans prouveur maison -- module faisabilite + tests #18954 MERGED 2026-10-03T14:38 (claim-AMEND ai-01:CoursIA-2 paths: agent_tests/prover/integration/**, Lean-10-LeanDojo.ipynb)
- carnet Lean-10-LeanDojo.ipynb present sur main
- module faisabilite integration leandojo v2 dans prouveur maison -> dossier agent_tests/prover/integration/ present sur main
- compatibilite Python 3.10 + deps mesuree -> verdict SOTA cmt 2026-10-03T02:00:57Z (myia-ai-01)
residue: followup_#19057 (LeanDojo-v2 volet A MERGED 2026-10-05, scoped sous [Lean] Intégrer LeanDojo-v2 : du traçage v1 de Lean-10 à la recherche de preuve (Pantograph) et au harnais prouveur #18430)
open-prs: 0
comments-reviewed: 3
[/CLOSURE PREFLIGHT]
— myia-po-2026:CoursIA-2, c.1408 — dispatch ai-01 msg-20261007T150526-ynzj1u
[INFO candidate-delivered] lane myia-po-2026:CoursIA-2 -- c.1429 -- confronte les 4 acceptances du [CLOSURE PREFLIGHT] (c.1408) a origin/main (eadde57).
Verification first-hand c.1429
- verdict SOTA etude faisabilite LeanDojo v2 -> PR feat(leandojo,#18915 pli 2): integration leandojo v2 dans prouveur maison -- module faisabilite + tests #18954 MERGED (commit 8f3bc5b feat(leandojo,feat(leandojo,#18562 pli 2): integration leandojo dans prouveur maison -- evaluation faisabilite #18915 pli 2): integration leandojo v2 dans prouveur maison -- module faisabilite + tests). Verdict SOTA documente au cmt 2026-10-03T02:00:57Z (myia-ai-01) : 4 axes RECOVERABLE-LOCAL, 1 axe INTRINSIC (torch/CUDA).
- carnet Lean-10-LeanDojo.ipynb sur main -> git ls-tree origin/main MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-10-LeanDojo.ipynb = blob present (sha 6f0372c8).
- module agent_tests/prover/integration/ sur main -> 3 fichiers : init.py (59d5bd93), leandojo_feasibility.py (e20f1a8389), test_leandojo_feasibility.py (b8fe59f80).
- compatibilite Python 3.10 + deps mesuree -> verdict SOTA cmt myia-ai-01 (RECOVERABLE-LOCAL : pip install lean-dojo 4.20.0 OK sans torch).
Statut
Tous les criteres du [CLOSURE PREFLIGHT] sont satisfaits sur main. Issue cloturable par coord ou adjoint.
Residu connu : followup #19057 (LeanDojo-v2 volet A MERGED 2026-10-05, scoped sous #18430) -- non bloquant pour la cloture de #18915.
Refs: PR #18954, cmt myia-ai-01 IC_kwDOH2Odns8AAAABa4Eqew, [CLOSURE PREFLIGHT] cmt 6040865186.
-- myia-po-2026:CoursIA-2, c.1429
[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
issue: 18915
verdict: CLOSE
acceptance:- Identifier les modules LeanDojo utiles, scope model only -> LIVRE : subset importable identifie (LeanGrepo, trace, is_available_in_cache, Dojo, Theorem, check_proof), verdict 5 axes rendu par myia-ai-01:CoursIA-2 le 2026-10-03T02:00Z (commentaire mesure firsthand Python 3.10.11 + lean-dojo 4.20.0)
- Valider compatibilite Python 3.10 + deps -> LIVRE : axe 1 RECOVERABLE-LOCAL (pip install lean-dojo OK, Requires-Python >=3.9,<=3.12 ; Python 3.14 non compatible documente)
- Notebook d'integration LeanDojo sur proof snippet -> LIVRE : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-10-LeanDojo.ipynb sur origin/main (73 cellules, 26/26 code executees) + Lean-10b-LeanDojo-v2-Pantograph-Lean-Python.ipynb ; module + tests : agent_tests/prover/integration/leandojo_feasibility.py et test_leandojo_feasibility.py
- Evaluer la portabilite sur les pre-conditions Lean 4 de CoursIA -> LIVRE : axe 4 RECOVERABLE-LOCAL conditionnel (toolchain lean 4 locale + reseau + cache), conditions enumerees dans le verdict
- Verdict SOTA parmi les 5 verdicts -> LIVRE : axes 1-4 RECOVERABLE-LOCAL, axe 5 INTRINSIC motive (torch/transformers ~2 Go non testables localement, plafond documente honnetement) ; PR feat(leandojo,#18915 pli 2): integration leandojo v2 dans prouveur maison -- module faisabilite + tests #18954 MERGED 2026-10-03T14:38:15Z
residue: none
open-prs: 0
comments-reviewed: 5
[/CLOSURE PREFLIGHT]
Fille de #18562 (pli 1 #18893 -- mode demo lean-dojo absent).
Cible : integrer LeanDojo (https://leandojo.org/leandojo.html) dans le prouveur maison de CoursIA. Sujet de la concern user sur #18893 : « est-ce qu’il est bien prévu comme discuté de rajouter la version 2 et d’évaluer la possibilité d’intégration dans notre prouveur maison? On veut voir tourner ça ».
Scope V2 :
Hors scope :
Lien : https://leandoge.org/leandojo.html
Ref: msg-20261002T...