Problems

Conjectures live in three layers. A problem is one informal question, with its own provenance and history. A statement is one precise proposition under a problem, addressable at its own /c/<id>/ URL, with (if any) exactly one Lean declaration attached – this is the atomic unit the site tracks status for. An area (along with model, form, and assumption class below) is a tag a statement carries, never a home directory: the pages under this section are generated views over the statements, not folders anything lives in. See the schema for the full frontmatter contract, or CONTRIBUTING.md for how to add one.

Browse

• All statements – the full sortable index, and where the Problems tab now lands.
• By Area – the same statements grouped by area, and by model, form and assumption class.

The status badge

Each statement carries one badge summarizing its formal/mechanized progress – a deterministic function of six fields tracked in the page’s status: frontmatter, never hand-picked. It’s deliberately narrow: it can’t say a result is settled before it’s machine-checked. category, status_summary, and the page’s own ## Status section carry the rest. See the status badge legend for what each symbol means and how to update one.

LaTeX templates

Writing up a new statement? Download the LaTeX templates – two small classes carrying the Conjura house style, plus an empty statement and solution built on them, so a new write-up doesn’t have to re-derive the preamble.