# Navigate Plectis Atlas as an agent

The website is agent-navigable using HTTP GET requests. No browser, account, JavaScript execution or installation is needed to read the map. This guide describes the same packets the human map uses; it adds no data fetch to human page loads. `llms.txt` is an optional discovery convention, not an access requirement or a guarantee about any crawler.

## Entry points

- [Concise entry](https://wcook04.github.io/plectis-atlas/llms.txt)
- [All families in static HTML](https://wcook04.github.io/plectis-atlas/explain.html)
- [Lean statements](https://wcook04.github.io/plectis-atlas/statements.html)
- [Sources and credits](https://wcook04.github.io/plectis-atlas/sources.html)
- [Counts and their definitions](https://wcook04.github.io/plectis-atlas/numbers.html)
- [Page sitemap](https://wcook04.github.io/plectis-atlas/sitemap.xml)
- [Repository instructions](https://github.com/wcook04/plectis-atlas/blob/main/AGENTS.md) and [source architecture](https://github.com/wcook04/plectis-atlas/blob/main/docs/ARCHITECTURE.md)

## Fetch the complete map

Fetch these two JSON packets to obtain all the map's nodes and relationships. Layout coordinates are unnecessary for research.

1. [Overview](https://wcook04.github.io/plectis-atlas/data/universe-data.json?v=c10632f78c45): `disciplines`, `families`, `links`, `sources`, `counts`, `catalogue_url` and `contract`.
2. [Parts](https://wcook04.github.io/plectis-atlas/data/universe-parts.json?v=c10632f78c45): `papers`, `results` and `lean`.

Both packets must have the same `generation_id`. This build uses `sha256:e44fe048bf34d4e55b76af0e42f931ce1121c5c189edf0e8cd6061a5902b3e47` from Statement Map, reading `openai/math` at `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb`. Check `contract[0].upstream_commit` in the overview. The query version is a cache key for the built packet bytes, not an archived snapshot. A generation mismatch detects different backend exports; it does not detect every rendering-only deployment. On a mismatch, reload this guide and both packets. For reproducible archival work, pin a repository commit and retain the packets together. Array indices are local to that packet set; store an object's `id`, never its array position.

The map contains 17 disciplines, 372 families, 719 papers, 1177 displayed results and 416 Lean statements. Displayed results include the headline selection and additional pairing targets; this is not every theorem-like environment in every paper. Follow each paper's page for its full text and conversion limits.

## Nodes and edges

Every node has a stable backend `id`: `d:` for a discipline, `f:` for a family, `p:` for a paper, `r:` for a displayed paper result, and `l:` for a Lean statement. Read names from `name`, `title`, `label` or the result's `kind` and `num`. A missing title or printed number remains unknown.

All numeric references below are zero-based array indices in the two packets fetched together:

| From | Relationship | Target |
|---|---|---|
| `disciplines[i].families` | contains | indices in `families` |
| `families[i].d` | belongs to | index in `disciplines` |
| `families[i].papers`, `.lean` | contains | indices in `papers`, `lean` |
| `papers[i].f`, `.results` | belongs to family; contains results | index in `families`; indices in `results` |
| `results[i].p`, `.f` | belongs to paper and family | indices in `papers`, `families` |
| `results[i].lean` | paper-to-Lean pairing | indices in `lean` |
| `lean[i].f`, `.results` | belongs to family; paired results | index in `families`; indices in `results` |
| `families[i].cites` | cites another family | pairs `[family_index, citing_paper_pair_count]` |
| `families[i].citedBy` | cited by another family | the reverse directed citation pairs |

`links` records the same family citations compactly as `[a, b, a_to_b_count, b_to_a_count]`. Each positive count is a directed citation between those family indices, measured in citing pairs of papers. A citation is not a proof dependency. A zero count means no edge in that direction.

Keep `lean[i].pairing` with a pairing edge. `candidate-pairing` is unreviewed. Keep `acc` as the attributed sources reporting accepted replays, not an Atlas verification claim. Read the family or Lean page for the precise evidence and limits.

Resolve each non-null `href` relative to `https://wcook04.github.io/plectis-atlas/`, including its fragment. Some nodes can have a null `href`; use the parent family or the paper's `pdf` instead of inventing a URL. Open a map node with `https://wcook04.github.io/plectis-atlas/#o=` followed by its URL-encoded `id`. Readable page URLs are preferable when a client cannot execute JavaScript.

## A small traversal

This standard-library example fetches the existing map packets and follows a family's papers, Lean statements and outgoing citations. Replace `f:159` with another returned family ID.

```python
import json
from urllib.parse import urljoin
from urllib.request import urlopen

base = 'https://wcook04.github.io/plectis-atlas/'
version = 'c10632f78c45'

def fetch(name):
    with urlopen(urljoin(base, 'data/' + name + '?v=' + version), timeout=30) as response:
        return json.load(response)

overview = fetch('universe-data.json')
parts = fetch('universe-parts.json')
if overview['generation_id'] != parts['generation_id']:
    raise RuntimeError('Deployment changed: reload agents.md and both packets')
family = next(row for row in overview['families'] if row['id'] == 'f:159')
print(family['id'], family['title'], urljoin(base, family['href']))
for kind in ('papers', 'lean'):
    for index in family[kind]:
        node = parts[kind][index]
        target = urljoin(base, node['href']) if node.get('href') else node.get('pdf')
        print(kind, node['id'], target)
for index, count in family['cites']:
    target = overview['families'][index]
    print('cites', target['id'], count, urljoin(base, target['href']))
```

For a selected family's extra wording, fetch `data/universe-detail-<d>.json` using its `d` index and check the generation. [Map search rows](https://wcook04.github.io/plectis-atlas/data/universe-search.json?v=c10632f78c45) offer names and result labels without downloading the separate full-text search shards. The [backend export](https://github.com/wcook04/plectis-atlas/blob/main/backend/EXPORT.json) identifies the source receipts; [source indexes](https://github.com/wcook04/plectis-atlas/tree/main/data) contain the extracted text and source locations. Respect their source, version, attribution and licence.

## Interpretation and contribution

Atlas is independent of OpenAI. It presents source records and attributed outside readings. It does not establish new mathematical results or equate a successful formal proof replay with a paper-to-Lean match. Paper conversions can be partial; the original PDF is the reference. Preserve unknown, candidate, unreviewed, withdrawn and source-attributed states when reporting findings.

Read [contribution instructions](https://github.com/wcook04/plectis-atlas/blob/main/CONTRIBUTING.md) before proposing changes. Signed contributions need the required human identity and review. An agent may report an unreviewed observation through the repository's dedicated form only when its operator and platform permit posting; reading this guide does not authorise a submission.