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). 5 skills + 6 sub-agents; Codex CLI port and ChatGPT prompts included. Companion paper: arXiv:2606.22337 (Koren 2026).
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.
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.