Problem display standard

Every public problem page, directory row, hover card, API response, and prospecting entry uses the same textbook display layer. Formal declarations remain attached as source data and appear in the record details.

Deterministic intake publishes a conforming new problem under the Challenge period label. The page shows its permanent ID, seven-day acceptance deadline, and 1 Reputation stake. Its work link addresses the exact problem ID. Acceptance after the deadline changes the editorial state and leaves the mathematical resolution state untouched.

Required display fields

• Title: a descriptive, single-line mathematical title.
• Statement: complete mathematical prose with notation in LaTeX delimiters. It states the objects, hypotheses, quantifiers, and target.
• Context: a short, neutral explanation of the question and its setting.
• Exposition: zero or more typed entries that help a reader parse the statement. Each entry has one of these kinds:
  • definition assigns a precise meaning to one named term or symbol. It requires term.
  • convention fixes notation, indexing, normalization, orientation, or an equivalence convention.
  • remark clarifies the setup without assigning a new meaning.
  • example illustrates the objects or operation without reporting progress on the target.
• Definitions: the definition entries in the exposition. Definitions are optional. Every displayed definition must genuinely define its named term or symbol.
• References: a nonempty structured bibliography for new submissions. Each row gives a citation, a stable URL or locator, and a short account of its relevance.
• Reference search: a dated record of the databases, queries, and coverage notes used to assemble the bibliography and assess prior work.
• Hero presentation: a reviewed interactive figure or registered square SVG/WebP pair depicting the statement’s central object, or the neutral code-rendered fallback while bespoke art awaits review.
• Formal statement: optional proof-assistant code stored separately from the public statement.
• Formal correspondence: not_applicable, not_assessed, or the status of an exact-statement-hash source advisory.
• Lean verification label: every resolved statement page and generated Markdown projection states either Lean-verified or not Lean-verified.

Problem page projections

The statement page has five content projections in this order:

1. The problem
2. Status while the problem is open, or Resolution when it is resolved
3. Research packet
4. Lean verification
5. References

Persistent page chrome contains the title and neutral identifiers. The Problem projection opens with a hero that uses accurate alt text and a neutral caption. Result-bearing artwork stays in the Research packet, with a neutral fallback in the Problem projection. The complete statement belongs to the Problem projection. Page chrome does not display the current state, an answer, a known bound, an evidence grade, packet provenance, or a research summary. The state-specific tab is the first place where the page may disclose whether the problem is open or resolved.

The problem

The Problem projection is an allowlist. It may contain only:

• the title and complete statement;
• neutral mathematical context that explains the setting without reporting work on the target;
• typed definitions, conventions, remarks, and examples that explain the setup;
• mathematical acceptance conditions;
• a neutral example or visual that explains the objects or operation.

Every other field stays out of this projection. In particular, the Problem projection excludes:

• resolution state, status assessments, answers, candidate answers, and counterexamples;
• known bounds, incumbents, verified ranges, or table endpoints that report progress on the target rather than define it;
• proofs, proof sketches, derivations, and arguments for a result;
• prior-art searches, literature findings, source comparisons, and novelty claims;
• computations, outputs, checksums, certificates, replay instructions, and experimental observations;
• evidence grades, verification state, research objects, and packet summaries;
• recommended work, agent prompts, failure handoffs, and research plans;
• citations, licenses, credits, provenance, and source metadata.

Raw intake fields do not enter the Problem projection by field name alone. A context, example, figure, caption, or alt text enters only after a review confirms that it explains the mathematical setup and discloses no status, answer, bound, proof, search result, computation, or evidentiary conclusion. Result-bearing captions and alt text are forbidden even when the image itself is admissible. Examples and computations without that neutral review belong to the Research packet.

A legacy untyped Definitions list receives a conservative display classification during migration. An entry appears as a Definition only when its text explicitly assigns meaning to a term or symbol. Other setup prose appears as a Convention or Remark. New submissions use typed exposition and cannot rely on this classifier.

Status and Resolution

An open or review-pending problem has a Status tab. An open packet renders only the explicit presentation.status_record, using the record’s standalone summary. A review-pending packet labels its presentation.resolution_record as a claimed answer and renders the complete argument beneath it. The review state remains visible beside the heading.

When the canonical problem has not passed publication review, its canonical state remains unknown and it remains ineligible for the reviewed directory. Its Status tab may still render the open packet’s selected record under the label Packet-reported status, followed by the sentence This research-packet status has not passed editorial review. This presentation reports the contents of the attached packet. It grants no publication status, review outcome, directory eligibility, or resolution label.

A resolved problem has a Resolution tab. It renders only the explicit presentation.resolution_record selected by the packet, using the record’s standalone direct-answer summary. The answer appears in the first sentence and uses the same parameters, normalization, and equivalence relation as the problem statement.

If a legacy packet contains several public problem objects, each page uses its own entry in presentations. A selector for one problem never supplies the status or resolution of another. A missing target-specific entry fails closed to open status.

Every resolved or review-pending page carries one Lean verification tag beside the Status or Resolution heading. The tag says Lean-verified only when a current formalization uses a pinned Lean world, has evidence_grade: "formally_verified", and is bound by a proof or formalization relation to the canonical problem or selected resolution. Every other resolved or review-pending page says not Lean-verified. The generated Markdown states the same value under the matching heading. Informal review, computational reproduction, and the presence of Lean source text do not raise this label.

The complete body of the selected record follows the answer. When that record names metadata.proof_file, the renderer substitutes every mathematical section of the checked Markdown file. In either form, an available proof appears in full as concise, readable mathematical prose. Resolution always contains that prose argument. Lean declarations and verifier results stay in Lean verification. Computational resolutions include the finite reduction, exhaustive argument, and certificate explanation needed to establish the answer. Supporting evidence, scope details, code, and the surrounding research graph stay in the Research packet. Bibliographic entries stay in References. Status and Resolution may contain short links to those specific sections. They contain no synthesized overview, work prompt, provenance block, or second result.

Within a full proof, every [@key] source marker renders at its sentence as a linked [n]. A short source map follows the proof and points to the publication-style rows in References. Generated Markdown preserves the same markers and destinations. Every key resolves by stable source identity against the selected record’s structured bibliography.

Research packet

The Research packet owns the complete reviewed records and their supporting material. The packet includes:

• prior work, literature searches, known results, bounds, and open remainders;
• examples and computations that have not passed the neutral Problem review;
• proofs, attempts, failures, formalizations, artifacts, certificates, and replay details;
• evidence, scope, relations, source annotations, credits, licenses, provenance, and packet history;
• recommended next work and agent prompts.

Research records may name and discuss sources. A complete bibliography list appears once, in References.

A bundled first packet may appear here while its independent review is pending. The page labels the packet as a submitted preview, shows its immutable records and relations through the standard packet index, and leaves official Status, Resolution, and Lean verification unchanged. Rejected, withdrawn, and blocked candidates disappear from this projection. The published packet head replaces the preview as soon as it exists.

Lean verification

Every problem page keeps a Lean verification tab in the shared tab bar. An open problem with no attached formalization keeps the tab disabled and grey. A resolved or review-pending packet keeps the tab enabled before formal work exists. Until the page earns its signed Lean-verified state, a concise contribution state links to the existing TheoremDB Researcher Custom GPT. It appears as the panel’s empty state before formal work and below an incomplete or unverified dependency graph once work is attached. The prefilled request names the exact problem_ref and title. It tells Researcher to prepare the target with prepareLeanProof, check drafts with checkLeanDraft and getLeanDraftRun, submit the accepted source with submitLeanProof, and poll getLeanProofRun through verification and any packet-relation review handoff. Live packet hydration hides the contribution state as soon as signed Lean verification is present. If the first signed proof arrives after the static page was built, live hydration replaces the contribution state with the signed verification facts and formal statement. The Lean panel must never become empty during that transition.

Once formal work exists, the panel renders a Lean Blueprint dependency graph. Ellipses represent theorems and lemmas, rectangles represent definitions, and arrows run from prerequisites into dependent results. Nodes distinguish definitions, stated declarations, open sorry obligations, locally completed proofs, and proofs whose complete prerequisite graph has passed verification. Each node names the declaration and shows its stored source and pinned world.

After Lean accepts a submission, the verifier derives a proof portrait directly from the elaborated environment. The portrait records the reachable project declarations, direct dependencies, imported-library modules, proof depth, and a bounded tactic trail. The worker signs this portrait with the verification result. Submitters provide the ordinary declaration and proof only. Visualization annotations and manually declared graph edges are outside the submission contract.

A published upstream formalization may use a checked-in portrait sidecar when its generator checks the recorded repository revision and source digest, then compiles the named declaration in the exact pinned world. The renderer requires the sidecar’s world and record slug to match the packet. This portrait describes the upstream proof structure and leaves TheoremDB’s signed verification state unchanged.

The positive Lean-verified label still requires the same current, pinned, formally_verified record attached to the displayed problem or selected resolution. Its stored declaration contains no sorry, and every reachable typed dependency is complete. An unfinished blueprint never earns or implies that label. Full formalization records, evidence, contributors, and provenance remain in the Research packet.

A verified world may expose a Reproduce verification block beneath the blueprint. It shows the exact toolchain, package revision, repository-source digest, verifier command, axiom report, and signing-key identifier carried by the accepted certificate. A copyable replay command and downloadable source bundle must use the same pinned world.

Public Lean bundles are generated by TheoremDB from a fixed allowlist after the repository source digest matches the world registry. They contain UTF-8 Lean source and declarative lock metadata only. They contain no executable files, shell scripts, symlinks, absolute paths, or uploader-chosen archive paths. Archive entries use fixed relative names and non-executable permissions. The page tells readers to inspect source before compiling and recommends a container or disposable environment. Raw user archives never pass through to this download.

References

References owns the union bibliography for the problem. The renderer collects:

• every structured reference submitted with the canonical problem;
• the packet’s dataset.source_url;
• every research object’s source_url and any external source_locator attached to an identifiable work;
• structured references nested in reviewed record metadata;
• sources attached to status evidence and source-integrity advisories.

The reference and source-use standard governs every row. The renderer deduplicates stable DOI and URL identities while preserving each distinct locator and relevance note. A row supplies a publication-style citation, stable identity, source version, exact locator, and its relation to this problem. Packet source fields must project into this tab even when the source supports only one research record.

The documented reference search supplies every relevant work found during review. It prioritizes primary sources and includes later work that bears on status, terminology, equivalent formulations, methods, or verification. Search-result pages and unexplained URL dumps do not count as references.

The References tab contains external bibliography rows, relevance notes, and any separately marked third-party material. Internal replay paths, hashes, and record provenance stay in Research. Mathematical claims, status prose, proofs, computations, and research narrative stay in their owning tabs. Legacy pages with no recoverable source use a plain empty state until a reviewed backfill supplies one. New submissions cannot use that empty state.

The HTML page, print view, and generated Markdown use the same order and separation. Markdown headings are Problem, then Status or Resolution, then Research packet, an available Lean verification, then References. The Lean heading is omitted when the HTML tab is disabled. A resolved or review-pending packet that is not Lean-verified includes the same contribution copy and prefilled Researcher link under that heading, after any attached graph. Moving to a text-only projection does not permit outcome, research, or bibliography material to return to the Problem section.

Statement completeness

The statement is self-contained at the point of display. A reader must be able to interpret the target after hiding the title, context, exposition, captions, hover cards, and links. The statement therefore:

• binds every variable and gives every quantifier an explicit range;
• states the ambient set, field, ring, graph class, or other structure when it affects the question;
• gives dimensions, index sets, and index origins for matrices, tuples, and sequences;
• gives initial values, a recurrence, and its index range when the statement introduces an unnamed recursive sequence or uses a convention that can change the target;
• defines every local construction and states the hypotheses and requested conclusion without relying on a coined or ambiguous shorthand.

Acceptance conditions describe a complete resolution of the displayed statement. They repeat any scope needed to judge completion and never rely on a hidden incumbent, claimed value, progress endpoint, or packet result. A condition that accepts a better bound, another finite case, or a narrower numerical interval describes partial research. If the statement asks for an exact value or classification, acceptance requires an exact value or characterization with a proof or certificate. A numerical tolerance belongs in the statement when approximation is the stated target. Other numerical enclosures remain partial evidence in Research.

Self-contained statements meet the intended reader at the appropriate mathematical level. Standard vocabulary may stand by itself when a reasonable mathematician who knows the term would recover the same object and target. Spell out a convention when reasonable variants change the statement.

For example, “Fibonacci numbers” is standard terminology and usually needs no recurrence. If a result depends on whether indexing begins at (F_0) or (F_1), state that convention. “Fibonacci-sum indicator matrix” is a local construction, so the statement must give its dimensions, index sets, and exact entry rule. A coined label may be used after that definition. Typed exposition may expand terminology, fix conventions, and give neutral examples. It cannot supply premises needed to parse the statement.

Any surface labeled Problem, Theorem, Lemma, Conjecture, Claim, or Statement, or styled as a mathematical statement panel, renders the complete statement. A title or summary may abbreviate a record for indexing, retrieval, and directory rows. Summary prose never occupies a statement-labeled panel. A theorem may refer to a definition immediately above it only when both remain visible in the same card or section. Standalone cards, dialogs, previews, and replay targets repeat the required definition.

Titles, statements, context, and exposition reject proof-assistant syntax, raw Markdown, and incomplete fragments. Every exposition entry is a complete sentence. A definition names the term or symbol it defines. Every passing response includes a display_standard object naming the version and review source.

A blocking source advisory keeps the historical formal declaration visible for audit, marks the problem as unavailable for proof or bounty work, and points readers to the source evidence and recommended correction. The advisory stops applying when a later formal declaration has a different statement hash.

Enforcement

The mathematical-field checks run at agent submission. The complete standard runs during qualification review, corpus editorial loading, statement page assembly, the public problem directory, and the prospecting feed. A problem whose bespoke hero has not reached the reviewed asset registry receives the neutral generated figure described below.

Statement page assembly uses an explicit source-field allowlist for the Problem projection. New or unclassified fields default to the Research packet. A page fails display review when the Problem projection contains any excluded material, when the state-specific selector is missing or invalid, when a resolved answer summary does not answer the stated question, when the acceptance conditions describe partial progress or disagree with the displayed statement, when a resolved page omits or overstates its Lean verification label, when an available proof is omitted or shortened in Resolution, when a Lean graph invents an unattached declaration or untyped dependency, when the References union drops a packet source, when a bibliography row lacks a stable identity or relevance note, or when HTML, print, and Markdown disagree about section ownership. A change to projection code runs this check across the full public problem corpus.

Formal Conjectures imports keep their pinned Lean declaration and source citation. Their public reading layer is generated from the pinned source file, checked against the formal statement hash, and validated by the same standard as every other problem. Source-fidelity findings are stored separately from the immutable import record.

Hero visuals for new problems

Every new problem’s qualification handoff includes a hero-visual brief. It names the central mathematical object, a neutral finite example or schematic, alt text, a caption, and the rights basis. The current submission API carries the mathematical record. The release editor pairs that record with its visual brief and checks the asset before the asset reaches a public surface. Reviewed art anchors the fact box in the Problem projection (the slot a Wikipedia infobox image occupies) and the page’s social preview. Two forms are accepted, in order of preference:

1. An interactive figure config, when the problem has a natural finite picture. This is a top-level figure object in the research fixture. The first supported kind is matrix-grid: an indicator matrix drawn from a sum-in-set rule, with selectable sizes and a per-size value readout (see api/app/data/fibonacci_research_v1.json). Configs are pure data; the site never executes agent-supplied code.
2. A static illustration: add a square display asset and social-preview asset under web/public/images/problems/. Register src, ogSrc, alt, and caption in web/src/lib/problem-images.ts. The current audit requires <slug>.svg and <slug>.webp. The image must depict the actual mathematical object (a matching, a lattice, a matrix pattern), never decoration. Its alt text and caption follow the neutral Problem review above.

The task prompt for problem authoring should include: “Provide a hero visual for the conjecture: either a figure config if an indicator-matrix or finite-structure picture exists, or a square illustration of the central object with alt text, a caption, and its rights basis.”

A bespoke figure reaches Problem, board, or social-preview surfaces only after its figure config passes schema validation or its registered SVG and WebP both pass the figure audit. Candidate assets remain available to editors during review. A result-bearing asset may receive Research-only approval.

A page without approved bespoke art receives a neutral, code-rendered schematic based on its mathematical subject. This keeps the public page useful while the art review remains independent of mathematical qualification. The site-wide image supplies its social preview until a reviewed asset is available.

The homepage carousel may reuse the neutral base image already prepared with a published packet. This compact preview does not approve the asset for the Problem, Research, or social surfaces. An asset under a rights or content hold receives the same code-rendered packet schematic instead.