r-irbe

@r-irbe source repo

66 skills
0 followers
6 hours ago last updated

▌
Lean Report · r-irbe
USE FOR: converting a Lean 4 project blueprint into a publication-grade LaTeX report — blueprint artifact ingestion (extracted LaTeX nodes, dependency DAG, JSON metadata), per-chapter narrative generation with mathematical prose, dependency-driven cross-referencing, figure generation (dependency graphs, module maps, coverage tables), and LaTeX → PDF compilation via the 6-stage INGEST → PLAN → NARRATE → ILLUSTRATE → ASSEMBLE → COMPILE pipeline. DO NOT USE FOR: generating the blueprint itself (use @lean-blueprint); writing one chapter without the pipeline (use @lean-doc-improvement); reviewing a finished report (use @lean-review-council); spec lifecycle (use @lean-specification). TRIGGERS: blueprint to report, generate report, latex pdf, project-report.tex, narrate chapter, dependency figure, blueprint compile.

0
installs
▌
Lean Gateway · r-irbe bundle
USE FOR: routing the top-level entry-point for a complex Lean 4 task; selecting which downstream skill(s) own each phase; preventing context collapse across long sessions; maintaining feedback / feedforward loops; fan-in / fan-out coordination; system-wide health monitoring. DO NOT USE FOR: doing any actual work (always delegate to a domain skill); single-file editing (use @lean-proof or @lean-doc-improvement); script-level enforcement (use @lean-enforcement). TRIGGERS: gateway, orchestrate, route, dispatch, top-level, context collapse, fan-out, fan-in, ecosystem health.

0
installs
▌
Lean Research · r-irbe bundle
USE FOR: per-question Lean 4 research — picking a research method (Mathlib grep / Web / repo grep / sub-agent), running the discovery ladder for Mathlib/Loogle/Reservoir/GitHub/literature lookups, choosing depth (Shallow / Standard / Deep / Exhaustive), emitting a findings + recommended-strategy + Zettel triple, integrating with the Rumsfeld epistemic matrix and the review council, running a typed protocol (M / T / L / S / D / X / E). DO NOT USE FOR: full council convocation (use @research-council); synthesis emission (use @research-synthesis-engine); package adoption or Lake dependency decisions (use @lean-package-research); proof writing (use @lean-proof); review (use @lean-review-council). TRIGGERS: research, mathlib lookup, find lemma, theorem search, Loogle, Moogle, Reservoir, package search, literature search, web search, what does X mean, typed research, M protocol, T protocol, L protocol.

0
installs
▌
Lean Blueprint · r-irbe
USE FOR: generating Lean blueprint, annotating theorems with @[blueprint], scaffolding blueprint directory, building blueprint LaTeX, rendering blueprint web. DO NOT USE FOR: writing Lean proofs (use @lean-proof), opening Lean/Mathlib PRs (use @lean-pr). TRIGGERS: blueprint, leanblueprint, LeanArchitect, dependency-graph.

0
installs
▌
Lean Enforcement · r-irbe bundle
USE FOR: running programmatic CI / pre-review / post-review gates for a Lean 4 project — axiom audit, council precheck, review coverage, metric sync, zettelkasten lint, bridge validation, proof quality, ecosystem health, workflow gate enforcement. DO NOT USE FOR: semantic / judgement review (use @lean-proof-review or @lean-review-council); orchestrating the broader QA lifecycle (use @lean-quality-engine); routing tasks across skills (use @lean-gateway). TRIGGERS: enforcement, CI gate, axiom audit, council_precheck, workflow_gate, ecosystem_health, sorry check.

0
installs
▌
Math Time Series · r-irbe
USE FOR: Time series analysis, signal processing, temporal pattern detection, and multi-scale temporal dynamics. Use for mathematical reasoning about time-varying data, smoothing, derivative estimation, spectral analysis, changepoint detection, and temporal trajectory computation. Covers both theory and computational methodology. DO NOT USE FOR: measure-theoretic / probabilistic basis (use @math-measure-probability); Lean proofs (use @lean-math-stochastic); nonlinear dynamics (use @math-nonlinear-dynamics). TRIGGERS: time series, signal processing, temporal pattern, multi-scale temporal, spectral analysis.

0
installs
▌
Research Council · r-irbe
USE FOR: orchestrating a 5-member Lean 4 research council (Α / Β / Γ / Δ / Ε) — RESEARCH loop (dual to RALPH), Rumsfeld epistemic mapping (known/unknown × known/unknown), cross-disciplinary research domains (Mathlib / AI / Physics / Bio / Social), session protocol, literature synthesis, self-improvement meta-loop. DO NOT USE FOR: single proof or single literature lookup (use @lean-research); proof review (use @lean-review-council); synthesis-only emission (use @research-synthesis-engine); proof itself (use @lean-proof). TRIGGERS: research council, RESEARCH loop, Rumsfeld matrix, epistemic mapping, research session, literature synthesis council, cross-disciplinary research.

0
installs
▌
AI Causal Deontic · r-irbe
USE FOR: Causal reasoning, counterfactual analysis, and deontic logic for AI systems. Use for formalizing cause-effect relationships (Pearl's hierarchy), interventional reasoning, structural causal models, counterfactual simulation, obligation/permission/prohibition reasoning, normative systems, and legal/ethical rule formalization in Lean 4. DO NOT USE FOR: formalising those models in Lean (use @lean-causal-reasoning); agentic AI behaviour (use @ai-agentic-evolving); commonsense reasoning (use @ai-commonsense-reasoning). TRIGGERS: causal, counterfactual, Pearl hierarchy, deontic, obligation, permission, structural causal model.

0
installs
▌
AI Symbolic Neuro · r-irbe
USE FOR: Symbolic AI, neuro-symbolic integration, knowledge representation and reasoning (KRR), ontology engineering, description logics, and hybrid symbolic-neural architectures. Use for reasoning about formal knowledge structures, rule-based systems, logic programming, semantic web technologies, and their integration with neural approaches in knowledge graphs and structured reasoning pipelines. DO NOT USE FOR: formalising the ontology in Lean (use @lean-knowledge-formalization); commonsense reasoning (use @ai-commonsense-reasoning); agentic AI (use @ai-agentic-evolving). TRIGGERS: symbolic AI, neuro-symbolic, knowledge representation, KRR, ontology engineering, description logic, hybrid AI.

0
installs
▌
Epistemic Mapping · r-irbe
USE FOR: mapping a domain's concept lattice, identifying load-bearing assumptions, surfacing implicit ontologies, drafting an epistemic terrain map. DO NOT USE FOR: producing formal proofs (use @lean-proof), gathering primary research data (use @applied-intelligence-analysis). TRIGGERS: concept-map, ontology, terrain, epistemic-survey.

0
installs
▌
Lean Doc Feedback · r-irbe
USE FOR: reviewing a Lean documentation draft, flagging undefined terms, suggesting cross-links, scoring readability against a rubric. DO NOT USE FOR: rewriting prose end-to-end (use @lean-doc-improvement), generating new blueprints (use @lean-blueprint). TRIGGERS: doc-review, readability, doc-feedback.

0
installs
▌
Lean Proof Review · r-irbe bundle
USE FOR: reviewing one Lean 4 proof / file for correctness, soundness, statement faithfulness, non-triviality, and proof quality; running the 4-layer verification checklist (formal soundness → statement → non-triviality → quality); flagging common Lean pitfalls; recommending tactic alternatives from the Mathlib + Aesop + Duper + Canonical stack. DO NOT USE FOR: writing a new proof (use @lean-proof); multi-agent council deliberation (use @lean-review-council); running CI scripts (use @lean-enforcement); scoring the whole project (use @lean-quality-engine). TRIGGERS: proof review, audit proof, verify Lean, 4-layer checklist, lean-pitfalls, proof quality.

0
installs
▌
Lean Zettelkasten · r-irbe
USE FOR: creating fleeting/literature/permanent ZK notes during Lean proof reviews, linking notes bidirectionally, running synthesis after a council session, detecting orphan and island notes, maintaining `_index.md` and `_tags.md`. DO NOT USE FOR: running the review council itself (use @lean-review-council), reviewing a single proof (use @lean-proof-review), updating external papers from results (use @lean-doc-improvement), authoring the review methodology retro (use @lean-retro-methodology), generating a project blueprint (use @lean-blueprint). TRIGGERS: zettel, ZK-, fleeting note, permanent note, synthesis.

0
installs
▌
Lean Pr · r-irbe
USE FOR: opening, titling, or labelling a PR against any Lean ecosystem repo (`leanprover/lean4`, `leanprover-community/mathlib4`, Cslib, or downstream projects), picking the right commit-message convention, applying upstream-specific labels (changelog-* for Lean core; t-* / easy / awaiting-author for Mathlib), running `lake exe mk_all` for Mathlib file renames, cross-linking dependent PRs. DO NOT USE FOR: in-tree proof review (use @lean-proof-review), Mathlib PR-review checklists (use `references/upstream/mathlib4-review.md`), writing the actual proof (use @lean-proof), building the change locally (use @lean-build), minimising an upstream-bug repro (use @lean-mwe). TRIGGERS: PR, pull request, "open a PR", changelog label, bors, maintainer-merge, `lake exe mk_all`, upstream filing.

0
installs
▌
Lean Math Analysis · r-irbe
USE FOR: real analysis, functional analysis, topology, and measure theory in Lean 4 / Mathlib — continuous functions, derivatives, integrals, metric / normed spaces, filter-based convergence, contraction mappings, convex analysis, spectral theory, and the real-valued bridges from a Nat-scaled model. DO NOT USE FOR: stochastic / probabilistic convergence (use @lean-math-stochastic); deterministic dynamical-system stability proofs (use @lean-math-dynamical); pure optimization (use @lean-math-optimization); typeclass-tower reasoning (use @lean-math-foundations); writing one specific proof (use @lean-proof). TRIGGERS: continuous, derivative, integral, metric space, normed space, filter, convergence, topology, measure space, contraction, Banach.

0
installs
▌
Lean Math Discrete · r-irbe
USE FOR: graph theory, applied lattice theory, combinatorics, DAGs, posets, provenance chains, dependency orders, lattice operations (severity / quality-gate / trust-vector / information-flow lattices), combinatorial bounds, and finite structures in Lean 4. Owns all applied lattice instances. DO NOT USE FOR: the abstract algebraic typeclass tower (use @lean-math-foundations); continuous structures (use @lean-math-analysis); writing one specific proof (use @lean-proof). TRIGGERS: graph, DAG, lattice, poset, combinatorics, provenance, dependency graph, severity lattice, knowledge graph, finite set bound.

0
installs
▌
Lean Specification · r-irbe
USE FOR: Design theorem specifications for Lean 4 proofs. Use when planning new theorems, lemmas, definitions, or tactics. Covers the three-part specification (requirements, design, documentation), lifecycle management, dependency analysis, and integration with the review council. DO NOT USE FOR: actual proof writing (use @lean-proof); requirement extraction (use @lean-doc-requirements); review (use @lean-proof-review). TRIGGERS: specification, theorem spec, three-part spec, lemma plan, tactic plan.

0
installs
▌
Lean Mwe · r-irbe bundle
USE FOR: creating minimal working examples (MWEs) from Lean 4 errors for upstream bug reports, capturing diagnostics with `#guard_msgs`, capturing panics with `#guard_panic`, running `lake exe minimize`, resuming long minimisations with `--resume`, verifying repros with `lake env lean`. DO NOT USE FOR: bisecting which Lean version introduced the bug (use @lean-bisect after MWE), building or validating the live project (use @lean-build), repairing the proof itself (use @lean-proof), filing the report (use @lean-pr after MWE + bisect). TRIGGERS: MWE, minimal repro, "minimise the error", "#guard_msgs", "#guard_panic", `lake exe minimize`, upstream bug report.

0
installs
▌
AI Agentic Evolving · r-irbe
USE FOR: Agentic AI systems, multi-agent coordination, evolving agents, agent lifecycle management, emergent behavior, and trust dynamics in autonomous systems. Use for reasoning about agent architectures, communication protocols, coalition formation, reputation systems, and the mathematical foundations of agentic safety and multi-agent trust formalization. DO NOT USE FOR: formal verification of those AI systems (use @lean-ai-formalization); high-stakes / verifiable AI mode (use @ai-high-stakes-verifiable); causal/deontic reasoning (use @ai-causal-deontic). TRIGGERS: agentic AI, multi-agent, evolving agent, agent lifecycle, emergent behavior, trust dynamics, autonomous system.

0
installs
▌
Lean Math Dynamical · r-irbe
USE FOR: nonlinear dynamical systems, Lyapunov stability, bifurcation theory, catastrophe theory, control theory, phase-portrait analysis, attractor classification, and any deterministic system with state evolution over time in Lean 4. DO NOT USE FOR: stochastic dynamics (use @lean-math-stochastic); pure analysis / topology (use @lean-math-analysis); optimization-only control problems (use @lean-math-optimization); writing one specific proof (use @lean-proof). TRIGGERS: Lyapunov, stability, bifurcation, cusp catastrophe, attractor, phase portrait, dynamical system, control theory, equilibrium.

0
installs
▌
Lean Quality Engine · r-irbe bundle
USE FOR: assessing overall Lean 4 project quality across seven dimensions (soundness, faithfulness, completeness, novelty, elegance, integration, documentation); preparing for milestones; orchestrating QA gates that wrap enforcement scripts, council reviews, coverage tracking, and health monitoring. DO NOT USE FOR: running a single enforcement script (use @lean-enforcement); reviewing one proof (use @lean-proof-review); council deliberation itself (use @lean-review-council); writing retros (use @lean-retro-methodology). TRIGGERS: QA, quality gate, milestone check, project health, qa-engine, quality score, QA lifecycle.

0
installs
▌
Lean Research Types · r-irbe
REDIRECT — the typed research protocols (M/T/L/S/D/X/E) previously hosted here have been folded into `lean-research` Part 9. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

0
installs
▌
Lean Review Council · r-irbe
USE FOR: orchestrating a 5-member Lean 4 proof review council (Σ Kernel Guardian, Φ Statement Oracle, Ν Novelty Scout, Λ Quality Architect, Ω Integration Sentinel); running RALPH (Review-Analyze-Learn-Plan-Handle) loops at member / council / project / meta scales; structured voting with structured-disagreement-resolution (SDR); council topology selection (Star / Pipeline / Mesh / Hierarchical / Swarm / Ring / Hub-Spoke); maximum-parallel agent dispatch with cascading completion handlers; specification lifecycle (requirements → design → docs); inter-council collaboration; Zettelkasten knowledge synthesis; calibration scoring; enforcement tactics. DO NOT USE FOR: reviewing one Lean proof in isolation (use @lean-proof-review); writing a proof (use @lean-proof); running CI scripts (use @lean-enforcement); single-skill council convocation when no multi-layer review is needed (use the relevant skill directly). TRIGGERS: review council, RALPH loop, council vote, SDR, council topology, kernel guardian, statement orac

0
installs
▌
Lean Doc Improvement · r-irbe
USE FOR: Update academic papers, technical reports, and documentation based on results from Lean 4 formalization. Use when formal verification reveals paper imprecisions, missing hypotheses, sharper bounds, new insights, or when metrics need synchronization. Covers paper appendix updates, verification tables, erratum entries, insight propagation, and metric synchronization between Lean and documents. DO NOT USE FOR: extracting requirements from papers (use @lean-doc-requirements); blueprint generation (use @lean-blueprint); report compilation (use @lean-report). TRIGGERS: update paper, doc improvement, paper revision, documentation update from Lean, doc-feedback consumer.

0
installs
▌
Lean Math Stochastic · r-irbe
USE FOR: probability theory, stochastic processes, Markov chains, time-series analysis, ergodic theory, row-stochastic matrices, mixing times, spectral gaps, stationary distributions, and any stochastic dynamics in Lean 4. DO NOT USE FOR: deterministic dynamical systems (use @lean-math-dynamical); abstract measure-theoretic typeclass plumbing (use @lean-math-foundations); pure topology (use @lean-math-analysis); writing one specific proof (use @lean-proof). TRIGGERS: probability, stochastic, Markov chain, time series, ergodic, mixing time, spectral gap, stationary distribution, row-stochastic, martingale.

0
installs
▌
Lean Nested Learning · r-irbe
USE FOR: Formalize and extend nested learning theory in Lean 4. Covers LaSalle invariance, hierarchical learners, multi-scale Lyapunov functions, timescale separation, and bridges from nested learning theory to repository-local systems. DO NOT USE FOR: proof tactics (use @lean-proof); Lyapunov-only proofs (use @lean-math-dynamical); review (use @lean-proof-review). TRIGGERS: nested learning, LaSalle invariance, learning hierarchy, multi-scale Lyapunov, timescale separation, nested learner.

0
installs
▌
Math Graph Knowledge · r-irbe
USE FOR: Graph theory, knowledge graphs, ontology engineering, provenance structures, network analysis, and formal knowledge representation. Use for mathematical reasoning about DAGs, KGs, trust networks, provenance chains, and any graph-structured knowledge. Covers both pure graph theory and applied knowledge graph methodology. DO NOT USE FOR: KRR / symbolic AI (use @ai-symbolic-neuro); causal DAGs (use @ai-causal-deontic); discrete math (use @lean-math-discrete). TRIGGERS: graph theory, knowledge graph, ontology, provenance, network analysis, formal knowledge representation.

0
installs
▌
Math Strategy Studio · r-irbe
USE FOR: Strategic mathematical thinking — brainstorming, problem decomposition, proof strategy design, creative hypothesis generation, and mathematical intuition development. Use when facing novel formalization challenges, when standard approaches fail, when exploring connections between domains, or when the theorem specification needs creative mathematical insight. The creative counterpart to the systematic research-council and review-council skills. DO NOT USE FOR: strategy analysis methodology generally (use @applied-strategy-analysis); research synthesis (use @research-synthesis-engine); Lean specification (use @lean-specification). TRIGGERS: strategy studio, brainstorming, problem decomposition, proof strategy, creative hypothesis, mathematical intuition.

0
installs
▌
Lean Build · r-irbe
USE FOR: building Lean 4 projects with Lake, validating Lean changes with `lake env lean`, picking targeted build commands (`lake build <Module>`), resolving stale build artifacts via `lake clean` + `lake exe cache get`, preparing CI-quality local checks. Applies to any Lake-managed project (Mathlib, Cslib, or downstream repositories). DO NOT USE FOR: bisecting which Lean version caused a regression (use @lean-bisect), minimising an error to a bug-report repro (use @lean-mwe), repairing the toolchain itself (use @lean-setup), writing or fixing the proof (use @lean-proof). TRIGGERS: build, lake, lake env lean, lake exe cache get, stale artifacts, lake clean, build error, CI prep.

0
installs
▌
Lean Proof · r-irbe bundle
USE FOR: writing Lean 4 proofs one tactic at a time, fixing tactic errors by priority, planning sorry placeholders, cleaning a working proof, resolving dependent-type rewriting failures. DO NOT USE FOR: reviewing existing proofs (use @lean-proof-review), project-wide quality assessment (use @lean-quality-engine), minimising an error into a bug report (use @lean-mwe), discovering tactics or API (use @lean-research), authoring new theorem statements (use @lean-specification), repairing toolchains (use @lean-setup). TRIGGERS: prove, tactic, sorry, unsolved goals, motive is not type correct.

0
installs
▌
Lean Setup · r-irbe bundle
USE FOR: bootstrapping a fresh leanprover/lean4 clone, repairing elan toolchains, linking stage0/stage1 builds, verifying that `lean` and `lake env lean` agree, cleaning up linked toolchains when done. DO NOT USE FOR: building Mathlib or downstream Lake projects (use @lean-build), bisecting a behavioural regression (use @lean-bisect), authoring a reproducer (use @lean-mwe), writing proofs (use @lean-proof), creating new lakefiles for downstream projects (use @lean-blueprint). TRIGGERS: elan, lean-toolchain, cmake preset, stage0, stage1.

0
installs
▌
Mathlib Pr · r-irbe
REDIRECT — Mathlib PR workflow has been merged into the agnostic `lean-pr` SKILL, with Mathlib-specific conventions extracted to `references/upstream/mathlib4-pr.md` (W4 Wave 2 / move A1 of lab/design/07-cluster-workflow.md). This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

0
installs
▌
Lean AI Formalization · r-irbe
USE FOR: Formal verification of AI systems — agentic AI safety, alignment, high-stakes AI, evolving agents, neural network properties, and AI governance constraints. Use when formalizing safety envelopes, trust dynamics, multi-agent composition, AI act compliance, reward specifications, alignment properties, or any AI system property that must be formally verified. DO NOT USE FOR: AI methodology itself (use @ai-high-stakes-verifiable or @ai-agentic-evolving); security-specific formalisation (use @lean-security-formalization); knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: AI formalization, agentic safety, alignment proof, high-stakes AI, neural network property, AI governance.

0
installs
▌
Lean Causal Reasoning · r-irbe
USE FOR: Formalize causal DAGs, knowledge graph quality gates, counterfactual reasoning, and provenance bridges in Lean 4. Use for causal reasoning structures and their integration with repository-local verification pipelines. DO NOT USE FOR: causal methodology not in Lean (use @ai-causal-deontic); knowledge graph formalisation generally (use @lean-knowledge-formalization); general AI formalisation (use @lean-ai-formalization). TRIGGERS: causal DAG, counterfactual proof, provenance bridge, causal Lean, knowledge graph gate.

0
installs
▌
Lean Competitive Math · r-irbe bundle
USE FOR: formalizing a Project-Euler / competition-math problem as a Lean 4 theorem that asserts a concrete numeric answer, proving it, verifying the answer actually computes (native_decide / #eval), then improving the proof from a compiler-trusted answer-check toward a kernel-checked or structural (closed-form) proof. Owns the answer-check-to-structural ladder (Bronze native_decide -> Silver decide / norm_num -> Gold characterising property / closed form) and its L3 non-triviality carve-out for legitimate native_decide answer-checks. Alias: euler-prover. DO NOT USE FOR: writing the theorem statement in isolation (use @lean-specification); one-tactic-at-a-time proof authoring or error triage (use @lean-proof); generic single-proof audit outside the carve-out (use @lean-proof-review); Mathlib API / lemma discovery (use @lean-research); project-wide quality scoring (use @lean-quality-engine); open problems with no known numeric answer (this skill requires a known target). TRIGGERS: Project Euler, competition ma

0
installs
▌
Lean Doc Requirements · r-irbe
USE FOR: Extract formal requirements from academic papers, technical reports, and design documents. Use when converting informal mathematical claims into Lean 4 theorem specifications. Covers claim extraction from LaTeX sources, equation identification, proposition mapping, hypothesis inference, and requirement traceability from document to formal specification. DO NOT USE FOR: paper update post-Lean (use @lean-doc-improvement); specification design (use @lean-specification); blueprint generation (use @lean-blueprint). TRIGGERS: doc requirements, requirement extraction, informal-to-Lean, claim extraction, paper-to-spec.

0
installs
▌
Lean Math Foundations · r-irbe
USE FOR: foundational mathematics in Lean 4 — Lean's type system (Prop / Type / universes), classical vs constructive choices, Mathlib's algebraic typeclass hierarchy (Group / Ring / Order / Lattice / Module / Algebra), category theory basics, and any proof that needs foundational reasoning about types, propositions, or universes. DO NOT USE FOR: applied lattice instances such as severity / quality-gate lattices (use @lean-math-discrete); analysis-flavoured algebra such as normed-space structure (use @lean-math-analysis); writing a specific proof (use @lean-proof); reviewing a finished proof (use @lean-proof-review). TRIGGERS: type universe, Prop vs Type, classical reasoning, Classical.choice, algebraic typeclass, Mathlib hierarchy, category theory, propext, funext.

0
installs
▌
Lean Package Research · r-irbe
USE FOR: Lean 4 package and toolchain research — evaluating Reservoir/GitHub packages, Mathlib/cslib pin changes, Lake dependency health, package adoption classes, update sequencing, and external theorem-substrate candidates. Use this whenever the user asks whether to add, update, fork, pin, vendor, or reject a Lean package, even if they phrase it as "can we use this repo?" or "does mathlib have this now?". DO NOT USE FOR: ordinary theorem lookup without a package decision (use @lean-research); package-file mutation or `lake update` execution (use @lean-enforcement plus a project-specific edit claim); proof writing (use @lean-proof); general project QA (use @lean-quality-engine). TRIGGERS: Lean package, Reservoir, GitHub Lean repo, Lake dependency, lake-manifest, lean-toolchain, mathlib update, cslib update, package adoption, package pin, dependency health, external theorem substrate.

0
installs
▌
Lean Tautology Triage · r-irbe
USE FOR: triaging Lean 4 theorem statements or proof sites that may be vacuous, tautological, smoke-test-only, reflexive-by-rfl, `: True` placeholders, bare `decide` closures, or automation-only proofs of supposedly substantive claims. Use this skill whenever proof review reports "vacuous", "tautology", "trivial", "placeholder", "smoke theorem", "rfl self-projection", "DEFINITE", or "HIGH" proof-quality risk. DO NOT USE FOR: ordinary proof writing (use @lean-proof); whole-project QA lifecycle (use @lean-quality-engine); running one enforcement script without interpretation (use @lean-enforcement); theorem search (use @lean-research). TRIGGERS: tautology, vacuous, trivial proof, smoke theorem, placeholder theorem, proof quality, `: True`, `by decide`, `by rfl`, rfl self-projection, suspicious automation, non-triviality audit.

0
installs
▌
Math Algebra Category · r-irbe
USE FOR: Abstract algebra, category theory, lattice theory, universal algebra, and algebraic structures relevant to Lean formalization. Use for reasoning about groups, rings, fields, modules, categories, functors, natural transformations, monads, adjunctions, lattices, and algebraic hierarchies. Covers both pure algebraic theory and categorical perspectives essential for type-theoretic formalization. DO NOT USE FOR: measure-theoretic reasoning (use @math-measure-probability); topology/analysis (use @math-topology-analysis); Lean proof (use @lean-math-foundations). TRIGGERS: abstract algebra, category theory, lattice theory, universal algebra, algebraic structure.

0
installs
▌
Lean Bisect · r-irbe
USE FOR: bisecting Lean 4 toolchain versions or commits to find which one introduced a regression, using `script/lean-bisect` with `#guard_msgs` / exit-code signatures, ignoring messages with `--ignore-messages`, bisecting between nightlies or arbitrary commits. DO NOT USE FOR: building a project (use @lean-build), minimising a Mathlib repro to a self-contained file (use @lean-mwe first), writing or fixing the proof itself (use @lean-proof), filing the bug report (use @lean-pr after the bisect points at a culprit). TRIGGERS: bisect, regression, "which commit broke", "behavior changed between", nightly bisect.

0
installs
▌
Lean Applied Reasoning · r-irbe
USE FOR: Applied reasoning for intelligence analysis, strategy creation and analysis, brainstorming methodologies, investigative reasoning, and domain-specific decision-making. Use when formalizing strategic frameworks, situational analysis, hypothesis generation workflows, decision-under-uncertainty models, or when connecting theoretical formalization to practical operational contexts. Bridges mathematical formalization to real-world application domains. DO NOT USE FOR: pure intelligence-analysis methodology (use @applied-intelligence-analysis); strategy analysis methodology (use @applied-strategy-analysis); legal reasoning methodology (use @applied-legal-reasoning). TRIGGERS: applied reasoning, intelligence formalisation, strategy formalisation, investigative reasoning, domain-specific reasoning.

0
installs
▌
Lean Math Optimization · r-irbe
USE FOR: optimization theory, convex optimization, game theory, reinforcement-learning theory (Bellman equations, value / policy iteration), Nash equilibria, minimax theorems, decision theory, and fixed-point iterations in Lean 4. DO NOT USE FOR: stochastic policies / Markov chains (use @lean-math-stochastic); pure analysis (use @lean-math-analysis); Lyapunov / control-stability proofs (use @lean-math-dynamical); writing one specific proof (use @lean-proof). TRIGGERS: optimization, convex, game theory, Bellman, value iteration, policy iteration, Nash, minimax, fixed point, KKT.

0
installs
▌
Lean Retro Methodology · r-irbe
USE FOR: running a Lean 4 corpus retrospective — RETRO protocol (Refactor-Extract-Test-Refine-Optimize), adapting to project scale (Solo / Small / Medium / Large), per-phase enforcement scripts, cross-skill optimization rules, retro personas, tracking documents, embedded RALPH inside RETRO phases. DO NOT USE FOR: single proof review (use @lean-proof-review); council convocation (use @lean-review-council); research (use @lean-research); enforcement gate execution alone (use @lean-enforcement). TRIGGERS: retro, retrospective, RETRO protocol, refactor extract test refine optimize, retro phase, retro session, corpus retro, cross-skill optimization.

0
installs
▌
Lean Retroactive Audit · r-irbe
USE FOR: Apply the review council system retroactively to an existing large Lean 4 project. Use when onboarding an existing codebase to the council review framework. Covers module discovery, dependency analysis, incremental audit scheduling, baseline establishment, gap analysis, and the catch-up RALPH cycle for bringing an existing project to full review coverage. DO NOT USE FOR: building a new council (use @lean-review-council); single proof review (use @lean-proof-review); RETRO methodology (use @lean-retro-methodology). TRIGGERS: retroactive audit, council onboarding, existing project audit, legacy Lean review.

0
installs
▌
Math Optimization Game · r-irbe
USE FOR: Mathematical optimization, game theory, decision theory, mechanism design, multi-objective optimization, convex optimization, and reinforcement learning theory. Use for reasoning about Bellman equations, Nash equilibria, Pareto optimality, gradient methods, linear/convex/integer programming, and optimization-related mathematics. Covers both pure theory and computational methodology. DO NOT USE FOR: Lean optimization proofs (use @lean-math-optimization); strategy methodology (use @applied-strategy-analysis); general nonlinear dynamics (use @math-nonlinear-dynamics). TRIGGERS: optimization, game theory, decision theory, mechanism design, convex optimization, reinforcement learning.

0
installs
▌
Math Topology Analysis · r-irbe
USE FOR: Point-set topology, functional analysis, real analysis, and topological methods for dynamical systems. Use for reasoning about continuity, compactness, fixed-point theorems, Banach spaces, metric spaces, convergence, and the topological foundations underlying Lyapunov stability, contraction mappings, and phase portrait analysis. DO NOT USE FOR: Lean analysis proofs (use @lean-math-analysis); algebraic structures (use @math-algebra-category); measure theory (use @math-measure-probability). TRIGGERS: point-set topology, functional analysis, real analysis, continuity, compactness, topological method.

0
installs
▌
Applied Legal Reasoning · r-irbe
USE FOR: Legal reasoning formalization — statutory interpretation, case-based reasoning, argumentation frameworks, defeasible rules, deontic norms, regulatory compliance, and their connection to provenance chains, governance structures, and formal verification for legal-adjacent AI systems. DO NOT USE FOR: formalising those legal models in Lean (use @lean-applied-reasoning); deontic reasoning specifically (use @ai-causal-deontic); security policy (use @applied-data-information-security). TRIGGERS: statutory interpretation, case-based reasoning, argumentation framework, defeasible rule, deontic norm, legal reasoning, regulatory.

0
installs
▌
Math Nonlinear Dynamics · r-irbe
USE FOR: General nonlinear dynamics, chaos theory, bifurcation analysis, catastrophe theory, attractor geometry, Lyapunov methods, phase portraits, and control-theoretic stability. Use for any mathematical reasoning about dynamical systems BEFORE or BEYOND Lean formalization. Covers theory, intuition, calculation techniques, and connections to phase portraits, catastrophe models, and governance dynamics. DO NOT USE FOR: Lean proofs in this domain (use @lean-math-dynamical); optimization theory (use @math-optimization-game); topology methods (use @math-topology-analysis). TRIGGERS: nonlinear dynamics, chaos theory, bifurcation, catastrophe theory, attractor, Lyapunov, phase portrait.

0
installs
▌
Math Product Management · r-irbe
USE FOR: Product management for mathematical formalization projects — roadmap creation, stakeholder management, feature prioritization for formal verification artifacts, theorem portfolio management, release planning, and the business/academic value analysis of formal proofs. Complements math-project-management (scheduling/execution) with strategic product thinking. DO NOT USE FOR: project-level scheduling (use @math-project-management); strategy methodology (use @applied-strategy-analysis); engineering discipline view (use @applied-engineering-disciplines). TRIGGERS: product management, roadmap, stakeholder management, feature prioritization, formal verification PM.

0
installs
▌
Math Project Management · r-irbe
USE FOR: Project and product management for mathematical formalization projects. Covers dependency-aware scheduling, risk management for unprovable theorems, progress tracking, milestone planning, resource allocation across proof workstreams, technical debt management, and stakeholder communication. Use when planning formalization campaigns, tracking multi-module efforts, or managing the intersection of research and engineering in formal mathematics. DO NOT USE FOR: product-level PM (use @math-product-management); retro methodology (use @lean-retro-methodology); engineering discipline view (use @applied-engineering-disciplines). TRIGGERS: project management, dependency scheduling, risk management for proofs, formalization PM.

0
installs
▌
Mathlib Build · r-irbe bundle
REDIRECT — Lake build content has been generalised and moved to the new `lean-build` skill (W4 Wave 2 / move A3 of lab/design/07-cluster-workflow.md). The Mathlib-specific `lake exe cache get` note survives in the new skill. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

0
installs
▌
AI Commonsense Reasoning · r-irbe
USE FOR: Commonsense reasoning for AI systems — world knowledge, naive physics, folk psychology, temporal/spatial reasoning, default reasoning, and their formalization. Use for reasoning about everyday knowledge that humans take for granted but AI systems need explicitly, especially when a downstream project must make implicit context explicit. DO NOT USE FOR: formal KR/ontology engineering (use @ai-symbolic-neuro); causal/deontic reasoning (use @ai-causal-deontic); formalisation in Lean (use @lean-knowledge-formalization). TRIGGERS: commonsense, naive physics, folk psychology, temporal reasoning, spatial reasoning, default reasoning.

0
installs
▌
Math Measure Probability · r-irbe
USE FOR: Measure theory, probability theory, stochastic processes, ergodic theory, and concentration inequalities. Use for mathematical reasoning about probability spaces, random variables, convergence, mixing, and probabilistic arguments. Covers both theoretical foundations and applied probabilistic methodology. DO NOT USE FOR: Lean proofs in this domain (use @lean-math-stochastic); time-series analysis (use @math-time-series); topology/analysis (use @math-topology-analysis). TRIGGERS: measure theory, probability, stochastic process, ergodic theory, concentration inequality, Radon-Nikodym.

0
installs
▌
Mathlib Review · r-irbe
REDIRECT — Mathlib PR review standards (attributes API, simp squeezing, normal forms, transparency, file size, naming/style URLs) have been demoted to `references/upstream/mathlib4-review.md`. Generic Lean proof review lives in `lean-proof-review`. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

0
installs
▌
AI High Stakes Verifiable · r-irbe
USE FOR: Formally verifiable AI, high-stakes AI systems, safety-critical deployment, certification, and regulatory compliance. Use for reasoning about AI systems that must be provably correct, auditable, or certifiable — medical AI, autonomous vehicles, legal decision support, military/intelligence systems, and mathematically rigorous AI governance. DO NOT USE FOR: formal verification proofs in Lean (use @lean-ai-formalization); agentic AI dynamics (use @ai-agentic-evolving); causal/deontic reasoning (use @ai-causal-deontic). TRIGGERS: high stakes, verifiable AI, safety critical, certification, regulatory compliance, AI assurance.

0
installs
▌
Applied Strategy Analysis · r-irbe
USE FOR: Strategy creation, analysis, and evaluation — game-theoretic foundations, competitive analysis, decision frameworks, SWOT/PESTLE, wargaming, and their mathematical underpinnings. Use for strategic reasoning about complex multi-agent scenarios, organizational strategy, research strategy, and mathematical planning for governance and optimization layers. DO NOT USE FOR: formalising strategic models in Lean (use @lean-applied-reasoning); intelligence analysis (use @applied-intelligence-analysis); game-theoretic optimization (use @math-optimization-game). TRIGGERS: strategy, SWOT, PESTLE, wargaming, decision framework, competitive analysis, game-theoretic strategy.

0
installs
▌
Lean Integration Protocol · r-irbe
USE FOR: Cross-skill integration protocol defining how all 39 skills work together. Covers the complete lifecycle from document to proof to document, inter-cluster communication, workflow templates for common tasks, and the master orchestration patterns. Use when coordinating multi-skill workflows or diagnosing cross-skill issues. DO NOT USE FOR: any single-skill execution (use that skill directly); the review council itself (use @lean-review-council); the gateway (use @lean-gateway). TRIGGERS: integration protocol, skill integration, cross-skill, skill lifecycle, inter-cluster routing.

0
installs
▌
Research Synthesis Engine · r-irbe
USE FOR: running the 5-role synthesis engine (Α-S Scanner / Β-S Clusterer / Γ-S Distiller / Δ-S Verifier / Ε-S Publisher) — Scan-Cluster-Distill-Verify-Publish (SYNTHESIZE) loop, four product tiers (Quick / Standard / Deep / Comprehensive), duality with the review-council RALPH loop, domain cross-references, Mathlib coverage tracking. DO NOT USE FOR: single-source literature review (use @lean-research); proof or formalization work (use @lean-proof or @lean-ai-formalization); review of a finished synthesis (use @lean-review-council); Zettelkasten card emission only (use @lean-zettelkasten). TRIGGERS: synthesis, SYNTHESIZE loop, synthesis council, Α-S, Β-S, Γ-S, Δ-S, Ε-S, scanner, clusterer, distiller, verifier, publisher, quick synthesis, deep synthesis.

0
installs
▌
Nightly Testing · r-irbe
REDIRECT — Lean/Mathlib nightly testing infrastructure notes (branches, tags, Zulip, mathlib4-nightly-testing fork) have been demoted to `references/upstream/lean-nightly-infrastructure.md`. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).

0
installs
▌
Epistemic Discovery Engine · r-irbe
USE FOR: epistemic discovery — picking a discovery mode (Census / Dependency / Literature / Cross-domain / Community), running an Unknown-Unknown (UU) hunting protocol at the right depth (Shallow / Standard / Deep / Exhaustive), emitting census + probe + trigger reports, anti-stagnation mechanisms, project relevance scoring. DO NOT USE FOR: a known research question (use @lean-research); council convocation on a known artifact (use @lean-review-council or @research-council); synthesis emission of known content (use @research-synthesis-engine). TRIGGERS: discovery, unknown unknown, UU hunt, epistemic discovery, census, dependency probe, cross-domain probe, community probe, anti-stagnation.

0
installs
▌
Lean Security Formalization · r-irbe
USE FOR: Data security, information security, access control, cryptographic properties, and privacy in Lean 4. Use when formalizing information flow policies, access control models, confidentiality/integrity/availability properties, data protection compliance (GDPR/LED), or trust model properties. DO NOT USE FOR: security policy design not in Lean (use @applied-data-information-security); AI safety formalisation (use @lean-ai-formalization); general knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: security formalization, information flow Lean, access control proof, cryptographic Lean, privacy proof.

0
installs
▌
Lean Knowledge Formalization · r-irbe
USE FOR: Knowledge representation, ontology engineering, symbolic AI, commonsense reasoning, causal reasoning, legal reasoning, and abductive inference in Lean 4. Use when formalizing knowledge structures, reasoning systems, argumentation frameworks, deontic logic, defeasible reasoning, or any domain where structured knowledge and inference must be formally verified. Core skill for knowledge-lifecycle and provenance architectures. DO NOT USE FOR: KRR methodology not in Lean (use @ai-symbolic-neuro); commonsense reasoning methodology (use @ai-commonsense-reasoning); causal/deontic methodology (use @ai-causal-deontic). TRIGGERS: knowledge formalisation, ontology in Lean, symbolic AI Lean, abductive inference Lean, legal reasoning Lean.

0
installs
▌
Applied Intelligence Analysis · r-irbe
USE FOR: Intelligence analysis methodology — structured analytic techniques (SATs), evidence reasoning, hypothesis generation, cognitive bias mitigation, competitive intelligence, and their formalization. Use for analysis of competing hypotheses (ACH), link analysis, timeline reconstruction, source reliability assessment, and connections to quality gates, provenance, and multi-agent trust. DO NOT USE FOR: formalising intelligence reasoning in Lean (use @lean-applied-reasoning); strategy analysis (use @applied-strategy-analysis); legal reasoning (use @applied-legal-reasoning). TRIGGERS: structured analytic techniques, SATs, evidence reasoning, hypothesis generation, cognitive bias, intelligence analysis, competing hypotheses.

0
installs
▌
Applied Engineering Disciplines · r-irbe
USE FOR: Engineering disciplines relevant to formal mathematical systems — control theory, systems engineering, reliability engineering, software verification, signal processing, and testing methodology. Use for bridging mathematical foundations to engineering practice, and for formalizing engineering requirements in Lean 4. DO NOT USE FOR: formal verification in Lean (use @lean-ai-formalization); security-specific engineering (use @applied-data-information-security); strategy analysis (use @applied-strategy-analysis). TRIGGERS: control theory, systems engineering, reliability engineering, software verification, engineering discipline.

0
installs
▌
Applied Data Information Security · r-irbe
USE FOR: Data security and information security formalization — CIA triad, access control models (BLP, RBAC, ABAC), information flow, cryptographic primitives, privacy (differential privacy, k-anonymity), threat modeling, and their formal verification in Lean 4. Use for security properties of provenance chains, trust composition, and multi-agent systems. DO NOT USE FOR: Lean formalisation of these policies (use @lean-security-formalization); engineering disciplines more broadly (use @applied-engineering-disciplines); legal-policy reasoning (use @applied-legal-reasoning). TRIGGERS: CIA triad, access control, BLP, RBAC, ABAC, information flow, cryptographic primitive, data security.

0
installs

66 published skills