# AGENTIC-Lea theorem-construction ladder

- **Registry ID:** `ic-lea`
- **Book:** Infinitesimal Creativity
- **Documentation status:** `local-curated`
- **Experimental status:** developmental and controlled theorem-prover studies
- **Canonical documentation URL:** https://categorical-ai.sridharmahadevan.com/experiments/ic-lea

## Purpose

Tool capability, scaffolded abstraction, fixed-vocabulary proof construction, structural repair, and early-stop tests.

## Book location

- Chapter 15: Mathematical Theory Construction

## Documented studies

- No study-level titles are registered; consult the family-level record.

## Associated code packages

- `synthetic-creativity-archive` — Infinitesimal Creativity registered experiment archive; **local-curated**; license decision pending. Registered, developmental, negative, and transport experiment directories underlying Chapters 10–19. Public packets require separate provenance, dependency, rights, and privacy review.
- `lea-upstream` — [Lea theorem prover](https://github.com/VIDA-NYU/Lea/tree/790853c89522bf5899feeb0052b795326feee720); **public-external**; upstream license. External Lean-based theorem-proving dependency used by the AGENTIC–Lea studies.

## Start here

These concrete files are selected from the complete resolved source surface. They orient the reader; they are not a claim that every family is independently reproducible.

- **runner · staged-not-public** — `synthetic-creativity-archive:agentic_lea_0/run_audit.py`. Locate this file in the curated companion packet; no public download is currently offered.
- **external-dependency · public-pinned** — [`lea-upstream:apps/lea-standalone/prover/examples/Ackermann.lean`](https://github.com/VIDA-NYU/Lea/blob/790853c89522bf5899feeb0052b795326feee720/apps/lea-standalone/prover/examples/Ackermann.lean). Open the pinned public source file.
- **runner · staged-not-public** — `synthetic-creativity-archive:agentic_lea_0/run_lea.py`. Locate this file in the curated companion packet; no public download is currently offered.
- **runner · staged-not-public** — `synthetic-creativity-archive:agentic_lea_1/run_audit.py`. Locate this file in the curated companion packet; no public download is currently offered.

## Entry points

- `packet scripts invoking Lea`

## Result artifacts

- `RESULTS.md`
- `RESULTS_QWEN.md`

## Resolved code surfaces (21)

- **external-dependency** — [`lea-upstream:apps/lea-standalone/prover/examples/Ackermann.lean`](https://github.com/VIDA-NYU/Lea/blob/790853c89522bf5899feeb0052b795326feee720/apps/lea-standalone/prover/examples/Ackermann.lean)
- **external-dependency** — [`lea-upstream:apps/lea-standalone/prover/examples/Logic.lean`](https://github.com/VIDA-NYU/Lea/blob/790853c89522bf5899feeb0052b795326feee720/apps/lea-standalone/prover/examples/Logic.lean)
- **external-dependency** — [`lea-upstream:apps/lea-standalone/prover/examples/StackMachine.lean`](https://github.com/VIDA-NYU/Lea/blob/790853c89522bf5899feeb0052b795326feee720/apps/lea-standalone/prover/examples/StackMachine.lean)
- **external-dependency** — [`lea-upstream:apps/lea-standalone/prover/examples/test_proof.lean`](https://github.com/VIDA-NYU/Lea/blob/790853c89522bf5899feeb0052b795326feee720/apps/lea-standalone/prover/examples/test_proof.lean)
- **runner** — `synthetic-creativity-archive:agentic_lea_0/extract_proposal.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_0/run_audit.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_0/run_lea.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_1/run_audit.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_1/run_followup.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_1/run_followup2.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_1/run_lea.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2/run_audit.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2/run_lea.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2b/run_audit.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2b/run_lea.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/freeze_stage_a.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/run_audit.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/run_stage_a.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/run_stage_a_followup.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/run_stage_a_followup2.py`
- **runner** — `synthetic-creativity-archive:agentic_lea_2c/run_stage_b.py`

## Frozen run records (5)

- `agentic_lea_0`
- `agentic_lea_1`
- `agentic_lea_2`
- `agentic_lea_2b`
- `agentic_lea_2c`

## Evidence boundary

Formal validity in a supplied or expanded language does not by itself establish mathematical creativity.

A code or artifact link establishes traceability. It does not by itself establish independent reproduction, statistical adequacy, correctness, or support for a claim beyond this boundary.