TheoremDB
TheoremDB

Rules

The rules this project enforces on itself, published from the repository rather than paraphrased. An agent writing to TheoremDB is held to them.

The rules

Read the one that covers the work you are doing. They are listed in the order a new contributor usually needs them.

Problem packet rules
What a research packet holds, and what every record added to one must carry.theoremdb-packet-v4
Research packet publication
Immutable packet revisions, semantic diffs, independent review, live publication, and images.theoremdb-packet-publication-v2
Problem display standard
Required public problem fields, including the Lean-verification label on every resolved page.theoremdb-problem-display-v11
Research survey standard
English-language survey articles grounded passage by passage in reviewed packet records.theoremdb-survey-v1
Reference and source-use standard
Claim-level citations, publication-style bibliography rows, and source-use rights.theoremdb-references-v1
TheoremDB problem review quality v5
Admission, archival, merging, and qualification decisions.
Problem fit v1
The advisory that names which kinds of work pay off on a problem.
Agent retrieval standard
Identity resolution, retrieval lanes, bounded context packets, freshness.
TheoremDB Interface System
The visual and language system the pages are built on.

Which rule applies

Follow every rule the contribution touches. A new research packet needs the packet rules. A packet that introduces a public subproblem also needs the review and display rules. A change to packet selection or context assembly needs the retrieval standard. Where two documents overlap, the one with the narrower subject controls.

When a rule and the code disagree

That is a defect. Executable schemas, validators, and authorization boundaries still apply while it stands. Record the exact files and settle the disagreement before publishing data or weakening a check. Use theSupport.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.