Skip to content

Grand Challenge Pedagogy Standard

Grand Challenge pedagogy is structural revelation under claim control. It exists to help a serious reader see the object, the obstruction, the support route, the proof boundary, and the next executable move.

Governing principle

Pedagogy is not simplification, decoration, or persuasion. It is part of mathematical governance.

This is the programme-wide teaching and exposition standard. It should be read with:

A document is pedagogically successful when a reader can answer five questions without inferring the author's intent:

  1. What object is being studied?
  2. Why does the object resist the naive route?
  3. What is the strongest supported claim?
  4. What has crossed a trusted boundary, and what has not?
  5. What finite action should happen next?

Rails before research

The current programme standard is rails before research.

Before adding a new doctrine expansion, Work Package, solver route, or visual artifact, the author must ask whether the existing stack can already carry the claim honestly.

Pedagogy must therefore make these rails visible:

Rail Reader-facing duty
source reconstruction preserve where the object came from and what was imported rather than audited
claim ledger state support class before rhetorical force begins
proof-debt register show what blocks promotion
fixture ledger prove that the process works on a bounded, inspectable example
resource budget bound expensive symbolic, search, and computational lanes
foundational profile state the carrier, ambient structure, axiom profile, witness policy, and pathology risk
certification route name the local statement that could be checked
accessible research guide show the prerequisites, first examples, first fixture, challenge ladder, and continuation graph

A beautiful explanation that hides one of these rails is not Grand Challenge pedagogy.

The nine-move exposition pattern

Every serious artifact should use this sequence. It may be compressed, but no stage may silently vanish.

  1. Status box. Say whether the artifact is exploratory, audited, computed, locally proved, certified, rejected, or superseded.
  2. Plain object. Introduce the mathematical object before machinery.
  3. Exact obstruction. Show the smallest mechanism that makes the naive route fail.
  4. Working model. Give a toy case, diagram, finite example, or local model that the reader can hold.
  5. Restricted claim. State the exact local claim under investigation.
  6. Theorem-spine location. Place the claim in the dependency graph.
  7. Support route. Present the proof, computation, certificate, replay, or negative result, with its support class.
  8. Debt and boundary. Separate what is proved, checked, open, imported, heuristic, or externally dependent.
  9. First executable step. End with one bounded action with input, output, and completion test.

Accessible research handoff

A serious mathematical artifact should not require a private mentor to reveal how to begin.

When a project is intended to recruit readers, collaborators, reviewers, or agentic assistants, it must include or point to an Accessible Research Guide. The guide supplies the missing on-ramp:

prerequisites
  -> first examples
  -> first fixture
  -> first local proposition
  -> challenge ladder
  -> certification path
  -> continuation graph

This is not a separate outreach layer. It is part of research integrity. A claim boundary that only experts can locate is still too easy to misuse.

The guide may be deferred only when the deferral is named in proof debt and has a completion condition.

External corpus quarantine

External datasets, scraped corpora, generated traces, benchmark labels, paper metadata, and source URLs are never programme authority on arrival.

Imported material must pass through this pedagogical quarantine:

external row
  -> preserved source object
  -> reliability register
  -> audited problem card
  -> route classification
  -> Work Package seed

The prose must not say that a problem is open, solved, or classified merely because a corpus field says so. Imported status is metadata until independently reconstructed.

Computation language

Every computation must be described in one of these classes:

Class What it permits
exploratory evidence candidate patterns and hypotheses
regression audit confidence that definitions, examples, and code paths still agree
exact finite verification a finite, explicitly bounded claim
certificate replay a local claim checked by a replayable artifact
formal proof a statement checked in a trusted formal environment
continuum proof a proof covering the full stated mathematical domain

Exact finite verification is not continuum proof. CAS output is not certification. A Lean statement with sorry is not a theorem. A visualization is not evidence unless the evidence is separately replayable.

Visual and mnemonic pedagogy

Visual artifacts, character roles, dashboards, diagrams, and app-like pages are welcome when they help readers organize the process.

They must obey three rules:

  1. They compress structure rather than replace it.
  2. They identify roles, boundaries, and routes.
  3. They never become proof-relevant by themselves.

The Minderlings are an example: they are mnemonic companions for readers, not authorities. Their value is that they help people remember which part of the stack discovers, organizes, certifies, maps, stewards, or maintains fixtures.

Semantic bridge discipline

A formal statement, exact certificate, or replay script is only as good as the semantic bridge connecting it to the intended human claim.

Pedagogy must therefore show:

  • the human statement;
  • the formal or computational statement;
  • the translation between them;
  • assumptions added or dropped;
  • model-class restrictions;
  • foundation and axiom-profile assumptions;
  • what would refute the bridge;
  • what would promote the bridge.

If the bridge is not yet checked, the artifact may be valuable, but the claim remains below certification.

Negative-result discipline

A negative result is complete only when it narrows the future.

Record:

  1. the attempted route;
  2. why it was plausible;
  3. the smallest exact failure;
  4. what the failure rules out;
  5. what it leaves viable;
  6. the next restricted target.

Do not write failure as atmosphere. Write it as geometry of the search space.

Review checklist

Before a page, Work Package, fixture, or route doctrine is merged, reviewers should check:

  • Does the page begin with status, not suspense?
  • Is the object visible before method?
  • Is the obstruction exact rather than atmospheric?
  • Is every computation classified?
  • Are imported claims quarantined?
  • Is the proof boundary explicit?
  • Is the semantic bridge named?
  • Is the foundational profile present or explicitly deferred?
  • Does the artifact include or point to an Accessible Research Guide when reader handoff matters?
  • Does the challenge ladder move from exercises to fixtures to restricted claims?
  • Does every visual or mnemonic artifact teach structure rather than claim support?
  • Is there a first executable step?
  • Would a skeptical reader know what could downgrade the claim?

Final compact

Grand Challenge pedagogy should leave the reader with this sentence completed:

We studied this object; the obstruction was this; the strongest supported claim is this; this part was checked; this part remains open; the next bounded move is this.

Anything less is not yet ready for serious mathematical handoff.