Erdős Frontier constellate · vfr_0a25edab

How the audit works

Method

Two axes, four trust tiers, and a signed event log you can replay without trusting this page.

The two axes

Axis 1, the proof. For each hosted Lean proof, a metaprogram loads the boxed-problem theorem in the proof’s own built environment and reports its axiom set (#print axioms), whether it is sorry-free, and the non-instance Prop hypotheses it takes as parameters. The last is the case an axiom check cannot see: a proof can be kernel-clean yet prove the goal only under a famous theorem passed as a hypothesis. Verdicts are mechanical and reproducible; no human or model is in this path.

Axis 2, the statement. Whether the formal statement faithfully states the boxed problem is a human judgment, not a machine one. Those verdicts are signed by a named reviewer with a registered key on the Vela frontier, and shown in the statement column. A problem with no signed verdict is left blank rather than assumed faithful.

The four trust tiers

Where a recorded claim and the machine tier disagree, the site marks the contradiction in cinnabar: recorded as solved, proof is conditional. Nine problems carry that mark today.

What it cannot do

When a proof file boxes more than one theorem, which declaration answers the problem can be a judgment call; the audit reads the problem-numbered theorem and records the declaration it used. It does not check that the statement is the right problem; that is Axis 2. It reports the conditionality of the proof available to it, which may differ from an informal argument recorded elsewhere.

Verify it yourself

The dashboard is a materialized view. The authority is a signed, replayable event log in the repository; you do not have to trust this page, the wiki, or us.

git clone https://github.com/williamjblair/erdos-frontier
cd erdos-frontier
vela check . --strict     # replay the signed frontier; any tampered event fails
vela frontier next .      # what is open to work on right now

The same state, three more doors: the hub index entry, re-derived from this repo by strict replay on every push; the reproduce walkthrough; and for agents, https://hub.constellate.science/mcp (MCP, streamable HTTP, read-only, no clone needed).

Cite the audit

loading…

Pin by commit for immutable citation; the event-log hash binds the signed verdicts you cite. Machine-readable feeds: verdicts.json (one row per problem), graph.json (the typed corpus graph), STATUS.md (maintainer view).