shuvomoy/autoopt

Run, resume, or coordinate a human-gated AutoOPT pipeline session for optimization-research automation inside a versioned research repository. Stages delegate to existing skills by name; Stage 0 repository grounding via research-repo-manager, Stage 1 numerical algorithm design via bnb-pep-skill, Stage 2 symbolic fitting of candidate formulas and proofs via frontier-llm-consult, which routes to the default external chatgpt-pro-session or an explicitly invoked native solve-with-highest-reasoning campaign with archived evidence, and Stage 3 Lean verification via lean-verify when available. Use when a researcher asks to orchestrate, chain, or gate these stages end-to-end, prepare a stage handoff, or close out a pipeline session with ledger updates. Every stage boundary requires explicit human approval; the skill automates the glue between stages, never the approvals; model outputs are candidates, never proofs.

Formalize, derive, and locally implement Branch-and-Bound Performance Estimation Programming (BnB-PEP) instances from math or plain English. Use when a researcher or agent needs worst-case performance analysis or stepsize/parameter optimization of fixed-step first-order methods via performance estimation problems (PEP), translating a function class, finite interpolation conditions, method update equations, performance measure, and initial condition into the Generalized BnB-PEP derivation and Julia/JuMP models for the primal SDP, dual SDP, and Stage 1/2 local nonlinear workflows. Covers smooth (strongly) convex, smooth nonconvex, weakly convex, Lipschitz, indicator/support-function, and composite/proximal OptISTA-style setups. Also covers explicitly requested BnB-PEP Stage 3 spatial branch-and-bound planning and static linting, while default generation remains Stage 1/2 only.

Package a full-workspace or directed file-selection handoff for attended ChatGPT Pro consultation through the Chrome plugin at chatgpt.com using GPT-5.6 Sol with Intelligence set to Pro, monitor by waiting in internal chunks of at most 60 seconds while inspecting the ChatGPT UI only roughly every 5 minutes after reasoning or generation visibly starts unless an error or ambiguous state is suspected, then import the response back into Codex. Use when the user wants Codex to prepare project or task context for ChatGPT's web UI through Chrome, then bring the response back into the local Codex workflow.

Persistent ChatGPT Pro workflow for starting, claiming, and continuing one reusable ChatGPT Web conversation with an initial project context bundle, monitored by waiting in internal chunks of at most 60 seconds while inspecting the ChatGPT UI only roughly every 5 minutes after reasoning or generation visibly starts unless an error or ambiguous state is suspected. Use when the user asks Codex to use ChatGPT Pro Session, keep working in the same ChatGPT Pro chat, reuse an already uploaded context bundle, claim an existing ChatGPT conversation URL as reusable context, request follow-up Pro analysis or diffs in the same session, or avoid repeatedly reuploading the same workspace context. Explicit invocation is standing consent to upload the initial selected context bundle to ChatGPT Web using GPT-5.6 Sol with Intelligence set to Pro; later implementation of Pro recommendations remains opt-in.

Human-gated frontier-model research router for AutoOPT Stage 2 symbolic fitting, candidate formula/proof discovery, proof planning, and independent model review. Use when Codex must choose between an external chatgpt-pro-session consultation and an explicitly invoked native solve-with-highest-reasoning campaign, preview external outgoing context or approve native repository scope, delegate to the selected route skill, archive durable evidence, and treat model outputs as candidate mathematical objects rather than proofs.

Formalize and verify optimization theorem, proof, and certificate targets in Lean/Lake using ChatGPT Pro blueprints only as proof-planning aids and local agentic Lean implementation as the execution path. Use for AutoOPT Stage 3, or standalone optimization-theorem verification, when Codex needs to turn detailed LaTeX/Markdown theorem proofs, symbolic fitting output, optimization certificate data, or an existing Lean/Lake project into checked Lean artifacts, repair proof scripts, build source-to-Lean project module graphs, and certify only what lake build verifies without sorry, axiom, admit, or unsafe; when feasible, close out with human-approved Challenge.lean/Solution.lean/config.json wrappers and comparator replay as additional evidence, including platform-specific closeout on Linux, native macOS, and Windows 11 WSL2.

Initialize, refresh, compact, and audit applied-math/optimization research repositories. Use when managing immutable sources, research goals, claim/evidence ledgers, experiment/reproducibility logs, source drift, next sessions, or approval-gated archiving.

Run an explicitly invoked, long-horizon native-Codex campaign on one exceptionally difficult mathematical or research problem using a user-confirmed minimum duration, the strongest currently available Codex GPT model, that model's highest supported reasoning setting, adaptive independent subagents, repository-grounded evidence, reproducible computation, and adversarial verification. Use only when the user explicitly invokes $solve-with-highest-reasoning for a configurable-duration highest-capability research campaign. Do not use for routine questions, ordinary proofs, generic brainstorming or planning, a bounded panel discussion, or external-model consultation.