mostlyharmfuleconometrics

mostlyharmfuleconometrics/lean-hansen-econometrics

Skill Claude CodeCodex

Run the repo's portable adversarial Lean review harness from Codex or another non-Workflow agent. Trigger when asked to use the review harness, review Lean files across redundancy/hygiene/faithfulness/proof-quality dimensions, follow review/README.md section (b), validate findings with review/worklist.py, or write…

mostlyharmfuleconometrics/lean-hansen-econometrics

Instructions file CodexOpenCode

AGENTS.md instructions for mostlyharmfuleconometrics/lean-hansen-econometrics, covering agent style guide, pr gate, core principles, 1. reuse mathlib first and 2. reuse repo theorems before adding new ones.