Maintainers: Moran Koren (Ben-Gurion University of the Negev, Economics)
Compatibility:claude-codecodex
Shared tooling for doing economic theory with LLMs — three bets on the same problem (machine help on a theorem you cannot already prove, with a trustable answer): math-proof (one careful single-shot pass), codex-math (OpenAI Codex as adversarial co-processor and hostile verifier), and co-math (a multi-agent proof-building project with strict unproven-gap flagging, reviewer sign-off gates, and optional Lean 4 verification, modelled on DeepMind's AI co-mathematician, Zheng et al. 2026). 6 skills + 6 sub-agents; Codex CLI port and ChatGPT prompts included. Companion paper: arXiv:2606.22337 (Koren 2026). Refresh 2026-09-29 (upstream at 2026-08-09): added the second-brain skill (agentic RAG over a local library of theory papers); re-copied the changed texts of math-proof (new proof-strategy planning section), co-math-init (standard workstream pipeline with readability pass), prover, coder and paper-reviewer (new gates against unverified reduction, complexity and integrality claims); corrected the codex-math source path to SKILL.md; nothing was removed. The 5 SKILL.md copies under codex/.agents/skills are the Codex port and are not catalogued separately.
Formalises a lemma in Lean 4 and verifies it with lake build — a green build is the strongest "proven" the system supports; the reviewer re-runs the build rather than re-checking the mathematics.
Python for computational exploration and numerical verification, with mandatory tests and golden values; cannot complete until tests pass and a reviewer accepts.
Post-verification exposition pass for already-verified proofs — six layers (architecture, signposting, justification, notation, intuition, grammar) without changing the mathematics.
Scaffolds a structured proof-building project (paper.tex, goals, decisions log, workstreams) with strict mode: every gap flagged unproven, nothing complete without reviewer sign-off.
Renders a compact status view of a co-math project — goals, active workstreams, blocked items, pending reviews, recent decisions — as an ASCII diagram.
Front door of a co-math project — reads goals.md, formalises research intent, dispatches and steers workstreams, filters low-level chatter from the user.
Sets up and queries an agentic-RAG second brain over a local library of theory papers, with LaTeX-aware ingestion, theorem and proof lookup, and hybrid search.
Single-pass discipline for full, gap-free proofs: state what you will show before showing it, sign every term, no "clearly", no overgeneralizing from examples.
Adversarial gate — a workstream cannot be marked complete until this agent writes an explicit approval file; cross-checks references, unproven blocks, and code-vs-claim consistency.