Schema

The frontmatter contract for statements and problems, for humans and agents

AICR has three content layers. Only the first two carry a schema; the third (facets) is generated, never authored. A fourth, much smaller kind of page – proposals – sits outside this layering entirely, for content that isn’t a problem, a statement, or a tag at all.

Statement frontmatter

Field Type Notes
id string Four-digit zero-padded, matches the c/<id>/ directory name.
problem string Exactly one hub slug under p/.
title string Precise, fully-quantified. Supports inline math with $...$.
short_title string For listing-table columns; falls back to title. Supports inline math with $...$.
pagetitle string Required when title contains math: its readable plain-text equivalent for browser tabs, search results and social previews. No TeX or HTML.
areas list of string Subset of the 19 fixed area slugs below. First entry is primary, display only – never a home directory.
model enum rom | prom | icm | ggm | qrom | standard | other
form enum separation | lower-bound | tight-bound | equivalence | impossibility | assumption | characterization
assumption_class enum unconditional | falsifiable | non-falsifiable
category enum research-open | research-solved | test | api | withdrawn. Solved special cases and sanity lemmas (research-solved, test) belong on the site – a disproof of an easy case is often the signal that a definition was formalized wrongly.
statement_sha string 64-char hex sha256 of the ## Statement tab content. Script-maintained by scripts/status_badge.py; never hand-edit.
revision integer Bumped automatically when statement_sha changes.
status map Six graded fields: statement_informal, statement_formal, statement_match, proof_informal, proof_review, proof_formal. Plus proof_direction (proves | refutes), optional, defaulting to proves: which way the work points. It is not a grade and never enters σ or π; refutes requires proof_informal != open. See the status legend.
status_badge string Generated. Never hand-edit.
status_summary string One required sentence, rendered next to the badge in listing tables. Supports inline math with $...$; see the convention below.
status_updated date
relations list of map {kind, target, note?}. kind is one of generalizes, specializes, implies, implied-by, equivalent-to, strengthens (same claim, better quantitative bound), variant-of, refutes, refuted-by, superseded-by. target is a four-digit id. note is required on an equivalent-to edge whose proof grades disagree.
lean map mode (in-repo | external-lean4 | other-system | none), plus repo/commit/path/decl/toolchain as applicable. commit is required once status.statement_formal != open when mode: external-lean4.
sources list of map {cite, url}. Real citations only – never a specific author/venue/year citation that hasn’t been verified to exist; leave the list empty rather than invent one.
withdrawn_reason string Required when category: withdrawn. Withdrawal keeps the page up as a tombstone that never 404s, together with a {kind: superseded-by, target: ...} relation pointing at whatever replaced it. It is the default way a statement leaves the listings; deletion is possible but conditional, and CONTRIBUTING.md carries the five conditions.

difficulty

Required, a mapping of three keys, and the only graded field on a statement that is not part of the badge.

difficulty:
  reach: new-idea        # routine | adaptation | new-idea | barrier
  by: ai                 # ai | human
  note: "one sentence saying what is missing, and checkable"

reach measures distance from known technique, not effort and not likelihood; the status legend says what each value means. by records who judged, on the same rule as status: a machine never writes human. note is required, because a grade with no stated reason cannot be argued with.

The 19 fixed area slugs

foundations, idealized-models, impossibility-results, symmetric-key, information-theoretic, side-channel, public-key, lattices, isogenies, quantum, zk, proof-systems, homomorphic-encryption, obfuscation, mpc, secret-sharing, universal-composability, privacy, consensus.

These are kept in sync between _quarto.yml’s sidebar and scripts/build_index.py’s AREA_SLUGS. Do not rename or merge them silently – see CONTRIBUTING.md.

Body sections, in order

  1. Badge markers (<!-- status:start -->...<!-- status:end -->), generated – the single combined ring+disc badge plus its one-line caption, at the very top of the page, before the tabset.
  2. A ::: {.panel-tabset} with ## Statement (the block statement_sha hashes), ## Proof, ## Formal Artifact.
  3. ## Open obligations – a markdown task list of the concrete outstanding items (unverified steps, unaudited files, unmatched formalizations, missing sanity lemmas). The open count feeds a listing column.

There is no rendered Status, Sessions, or Changelog section on the page.

status_summary is still a required frontmatter field (it’s what shows next to the badge in listing tables), it’s just not restated in page prose – the badge’s own caption is the brief explanation shown on the page itself. The same single combined badge (ring and disc together) is used everywhere: in the frontmatter’s status_badge field, at the top of the page, and in every listing table. Session dumps still live in each leaf’s sessions/ folder for provenance (excluded from the site); revision history is tracked by revision/statement_sha and by the commit that changed them – see CONTRIBUTING.md for the same-id-vs-new-id rule and where a misformalization classification belongs.

See _templates/statement.qmd for a fully commented skeleton.

Mathematics in titles and summaries

Write mathematical expressions in title, short_title and status_summary as inline LaTeX inside $...$, just as in the main text. Use a folded YAML scalar (>-) so that backslashes are preserved and source lines can wrap without adding line breaks:

title: >-
  A Protocol Using $O(\tau)$ Bits
short_title: >-
  $O(\tau)$-Bit Protocol
pagetitle: "A Protocol Using O(tau) Bits"
status_summary: >-
  Known constructions use $O(\tau)$ bits; the target is $\tau + o(\tau)$.

When the full title contains math, provide pagetitle as a readable plain-text equivalent. It supplies browser and social metadata; a post-render step also uses it for search-result titles. For powers, write $2^{-128}$ in title and 2^(-128) in pagetitle. This avoids raw TeX in places that cannot typeset it. If only short_title contains math, pagetitle is optional.

Put complete expressions inside the delimiters, including Greek letters, subscripts, powers, inequalities and asymptotic notation. For example, use $\tilde{O}(n^{1/2})$ instead of O~(n^{1/2}). Leave prose outside math and use inline math only, without spaces immediately inside the dollar delimiters. Do not infer or change a claim while converting its notation.

build_index.py rejects malformed delimiters, unbalanced TeX braces, decoded line breaks and control characters, and warns about likely unmarked notation. Folded YAML >- joins source lines into a single paragraph; literal line breaks in a parsed field can instead indicate a corrupted TeX escape. Warnings require editorial judgment and do not block the build. After rendering, summary_math.py --site _site requires every configured listing page, checks its rows against the generated index, and requires exactly one summary per row. The all-statements index must also match the browsable source statements. It checks that summary and listing-title formulas preserve the source TeX, that each statement page has exactly one title heading with the expected formulas, and that MathJax is included where needed. When pagetitle is supplied, browser/social metadata and all matching search-result titles must agree with it (with the site name added to browser tabs). It does not check the truth of the mathematics or replace browser checks of typesetting and pagination.

What the badge gate scans

scripts/status_badge.py scans c/ and papers/ by default, and CI runs it as --check c papers. A paper under papers/ carries the same badge contract as a statement – the same status: fields, the same hashed ## Statement tab, the same generated status_badge – so the same staleness gate applies to it.

Hubs under p/ are not scanned. A hub carries no badge of its own, only an aggregate view over its children, so it has no status: block for the script to grade. Pages without a status: block are skipped in any case; naming the two roots explicitly is about intent, so that putting a status: block on a hub is a deliberate schema change rather than something the script quietly starts generating a badge for.

Problem frontmatter

Just title and an optional subtitle. The body carries motivation, provenance/history, a parameter lattice (a table whose axes are the independent dimensions the family varies along, each cell linking to the occupying leaf, empty cells marked unstated as research prompts rather than left blank), and a listing of the hub’s own children. See _templates/problem.qmd.

Machine-readable index

scripts/build_index.py emits aicr.json at the site root: every statement, keyed by id, with its full frontmatter, parsed obligations, and resolved relations. This is generated (gitignored, rebuilt by CI before every render) – read it, never hand-edit it. It’s the interface external tooling (for example a proof-campaign harness) consumes as a work queue.

Identifier and revision rules

See CONTRIBUTING.md for the full editorial rule on when a change needs a new id versus a revision bump on the same one.