# Repository Map

This file explains which parts of the repository users are expected to edit and which parts are mainly runtime or AI-managed.
For setup and operational workflows, use this together with [`GETTING_STARTED.md`](GETTING_STARTED.md) and [`USER_GUIDE.md`](USER_GUIDE.md).

## Edit Here First

| Path | Main owner | Manual edits | Purpose |
| --- | --- | --- | --- |
| `AutomatedTheoryConstruction/Theory.lean` | User | Recommended | Public entry point for the active theory |
| `AutomatedTheoryConstruction/Theory/*.lean` | User | Recommended | Supporting definitions and lemmas imported by `Theory.lean` |
| `AutomatedTheoryConstruction/research_agenda.md` | User | Recommended | Persistent value guidance for what kinds of problems the system should prefer |
| `materials/` | User | Recommended | Organized deep-research outputs, literature summaries, and source-link bundles used as optional external context |
| `AutomatedTheoryConstruction/seeds.jsonl` | User / AI | Allowed | Initial open problems; may be user-provided or regenerated |
| `prompts/*.md` | User | Allowed | Worker prompt behavior and output guidance |
| `configs/atc.json` | User | Allowed | Runtime configuration |

## Usually Generated By The System

| Path | Main owner | Manual edits | Notes |
| --- | --- | --- | --- |
| `AutomatedTheoryConstruction/Derived.lean` | AI | Allowed but not preferred | Accumulated verified theorems; often overwritten or extended by the loop |
| `AutomatedTheoryConstruction/Scratch.lean` | AI | Not recommended | Temporary Lean verification target |
| `data/loop/open_problems.jsonl` | AI | Not recommended | Active solver queue |
| `data/loop/archived_problems.jsonl` | AI | Not recommended | Archived low-priority or repeatedly failed problems |
| `data/loop/solved_problems.jsonl` | AI | Not recommended | Solved problem log |
| `data/loop/counterexamples.jsonl` | AI | Not recommended | Counterexample log |
| `data/loop/formalization_memory.json` | AI | Not recommended | Retry/history memory |
| `data/loop/theory_state.json` | AI | Not recommended | Latest global theory summary, current next-direction bias, and compact research-agenda summary |
| `data/refactor/` | AI | Do not edit | Refactor reports, dependency snapshots, and chunk plans |
| `data/runs/` | AI | Do not edit | Run artifacts and logs |

`materials/` is intentionally not part of the runtime state schema.
Use it to store organized deep-research notes and literature context that should remain external to `data/loop/theory_state.json`.

## Shared Or Advanced

| Path | Main owner | Manual edits | Purpose |
| --- | --- | --- | --- |
| `scripts/` | Shared | Advanced only | Orchestration, worker wrappers, verification, and state updates |
| `scripts/lean_verify.py` | Advanced | Usually do not edit directly | Verification execution entrypoint; set `ATC_PROOF_EXECUTOR` instead of editing code for custom checkers |
| `LeanTools/` | Shared | Advanced only | Standalone Lean helper tools used by dependency extraction and pass 1.5 rewrites |
| `Makefile` | Shared | Allowed | Thin wrapper around the CLI |
| `tests/` | Shared | Allowed | Smoke tests and repo-level checks |
| `README.md` | Shared | Allowed | User-facing entry point |
| `design/` | Shared | Allowed | Design notes and runtime details |

## Usually Do Not Edit

| Path | Reason |
| --- | --- |
| `.lake/` | Lean and Lake dependency/build artifacts |
| `build/` | Generated build output |
| `.venv/` | Local Python environment |
| `lake-manifest.json` | Dependency lockfile; change only when intentionally updating dependencies |
| `example/` | Reference examples, not the active runtime theory |

## Short Version

If you want to know where to start:

1. Edit `AutomatedTheoryConstruction/Theory.lean`.
2. Add local theory files under `AutomatedTheoryConstruction/Theory/` if needed.
3. Edit `AutomatedTheoryConstruction/research_agenda.md`.
4. Run `make build` and then `make check-scratch`.

If you are trying to customize the system rather than the theory:

1. Edit `prompts/*.md` to change AI behavior.
2. Edit `configs/atc.json` or `Makefile` to change runtime settings.
3. Edit `scripts/` only when changing the implementation itself.