Issue #59 owns publishing LeanCategories to Prove2Me. Verified 2026-09-10 against prove2.me/skill.md, references/contribute.md, GET /api/v1/environments, and the anthropics/fermats-last-theorem export. Platform: definitions are full Lean files via POST /api/v1/submit-definition, name [a-zA-Z_][a-zA-Z0-9_]* unique per environment and permanent (no delete or code re-upload); imports resolve only against Mathlib and published Definitions.Def_ / Theorems.Thm_; 300 s compile cap; 100 pending jobs; private:true stages. Default environment Lean v4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; the corpus builds there unchanged. Working standard from the FLT export: definition files keep API lemmas (1,117 of 1,451 Def files hold theorems, 16,237 total); every reusable result is a card, one theorem per Thm file, proof in a separate Sol module. Card criterion for this repo: referenced from another module (282) or realizes a numbered source result. Corpus has 12 axiom stubs in Catalogue/Realization.lean with 18 downstream modules, excluded until #31/#33. openai/NavierStokesAndEuler uses the Comparator/formalization.yaml (Palomar) layout, not Prove2Me.