This repository contains the user skills and Lean verification code for the following paper:
Heechang Kim, Ernest K. Ryu, Shuvomoy Das Gupta, "A Domain-Specific Harness for End-to-End Automation of Optimization Research", 2026.
A preprint of the work is available on arXiv at the link: https://arxiv.org/abs/2608.07407.
If you find the code helpful in you project, we kindly request that you cite the following paper:
@misc{AutoOPT2026,
author = {Kim, Heechang and Ryu, Ernest K. and Das Gupta, Shuvomoy},
title = {A Domain-Specific Harness for End-to-End Automation of Optimization Research},
year = {2026},
archivePrefix = {arXiv},
eprint = {2608.07407},
primaryClass = {math.OC},
}
Skills/ contains the eight skills used by the AutoOPT framework.
The main skills are:
| Skill | Role |
|---|---|
auto-opt |
The main pipeline |
research-repo-manager |
Skill for maintaining the research repository |
bnb-pep-skill |
Stage1 of AutoOPT to run BnB-PEP methodology |
frontier-llm-consult |
Stage 2 of AutoOPT to find an analytical form of the algorithm + convergence proof |
lean-verify |
Stage 3 of AutoOPT for Lean formalization |
The main skills use the following additional skills:
| Skill | Role |
|---|---|
chatgpt-pro-handoff |
Auxiliary skill |
chatgpt-pro-session |
Auxiliary skill |
solve-with-highest-reasoning |
Auxiliary skill |
Lean-Related/ contains two projects pinned to Lean 4.32.0
and mathlib 4.32.0:
LemniAccformalizes the discrete and continuous lemniscate-acceleration results, including its recurrence, Lyapunov, convergence, interpolation, and lemniscatic components.ITEM-fformalizes the analytic ITEM-f construction, algorithm, model, Lyapunov argument, and convergence result.
Each project includes its Lean source, pinned Lake environment, theorem-facing
Challenge.lean and Solution.lean wrappers, and an AxiomAudit.lean target.
Miscellaneous/Self-contained analytical proofs. Selfcontained-PEP-proofs-for-Lemniscate-and-Itemf/ folder located in the Miscellaneous folder
contains self-contained PEP-based convergence proofs for lemniscate acceleration and ITEM-f. These documents are self-contained: they state the algorithms and rates, construct their parameters,
formulate the corresponding PEPs, and give the analytical dual certificates
and their feasibility proofs. Note that in the paper we provide the slightly more compact proofs based on Lyapunov analysis.
To run AutoOPT we first need to install a few prerequisites first. We can install AutoOPT skills in two ways: (i) by installing the skills manually, (ii) by installing the AutoOPT plugin (new!).
AutoOPT requires a few runtime prerequisites or tools. You can either install them before installing AutoOPT, or install AutoOPT first, and then from the agent (e.g., Codex) just ask it to install the prerequisites, e.g., say something like For using AutoOPT smoothly what are the tools that should be installed? Please show me the list and upon my approval, please install them.
The prerequisites are:
- OpenAI Codex (or a similar agent)
- Python 3.10 or newer (installing common popular packages like NumPy, SymPy can be helpful)
- Julia 1.10 or newer, and Julia packages JuMP, Ipopt, Clarabel, Mosek, Gurobi, KNITRO (note that commerical solvers Mosek, Gurobi, KNITRO are optional)
- Chrome extension Codex (or browser extension the agent in consideration)
- Lean, Lake, the required mathlib project
- Comparator or Landrun tooling
- Optional but recommended: Wolfram Mathematica or Wolfram Engine for symbolics. Though SymPy suffiices in many cases.
The easiest way is actually just downloading the repository locally on your computer, start Codex (or whatever agent that you like) from that folder and then ask Codex to install the skills located in the Skills folder!
If you like doing things manually, then please copy or symlink the required directories from Skills/ into a location scanned by your agent. For Codex, use $HOME/.agents/skills/ for user-wide installation or <repository-root>/.agents/skills/ for repository-scoped installation; for Claude Code, use ~/.claude/skills/ for user-wide installation. In Codex CLI or the IDE extension, run /skills to confirm discovery, invoke a skill as $skill-name, and restart Codex if an installed skill does not appear.
We have made a plugin for Codex based on the new plugin standard. However please keep in mind that plugin is a very recent open standard (Aug 7, 2026), and may be rough around the edges!
The packaged autoopt plugin is the portable installation for the Codex app and CLI. Codex plugin availability does not include the IDE extension. From any directory, run these two commands to install the plugin directly from this GitHub repository:
codex plugin marketplace add https://github.com/Shuvomoy/AutoOPT
codex plugin add autoopt@autooptThe first command asks Codex to fetch and register the marketplace stored in this repository. The second command installs the autoopt plugin from that marketplace. Then Verify the installation:
codex plugin list --marketplace autoopt --jsonStart a new Codex task so that the installed plugin is loaded, then invoke the pipeline with:
$autoopt:auto-opt
Each project uses its checked-in lean-toolchain and lake-manifest.json:
cd Lean-Related/LemniAcc
lake buildcd Lean-Related/ITEM-f
lake buildPlease report any issues via the Github issue tracker. All types of issues are welcome including bug reports, feature requests, and so on.
Please feel free to send an email 📧 to sd158@rice.edu regarding any subject including but not limited to comments about this codebase/paper, or just to say hi 😃!