Mathematical Strategy Atlas

A scorer for formal-math proof-search hypotheses

mathematical_strategy_atlas_hypothesis_scorer is a small component that records a formal-math proof search's first move before any proof runs. mathematical_strategy_atlas_hypothesis_scorer is a small component that records a formal-math proof search's first move before any proof runs. It reads public problem feature tags and a strategy atlas, scores each candidate opening strategy, and writes down which one it picked and why. It never proves anything.

The output is a set of result records: the selected strategy id for each case, the integer score that chose it, the component breakdown that produced the score, and a list of cases where nothing matched. The output is a set of result records: the selected strategy id for each case, the integer score that chose it, the component breakdown that produced the score, and a list of cases where nothing matched. A cold reader can take the same three input files and re-derive every selection by hand.

The shipped finite-sum example

A worked example: a problem tagged iff_goal scores the iff_split strategy highest and selects it. A worked example: a problem tagged iff_goal scores the iff_split strategy highest and selects it. A problem whose only tag matches nothing scores no candidate above zero and resolves to a typed STRATEGY_SELECTION_MISS instead of a silent guess.

Purpose

A proof search has to start somewhere. Before a premise is retrieved or a tactic is run, an agent has already committed to a first move: a goal shape and a family of tactics it expects to use. A proof search has to start somewhere. Before a premise is retrieved or a tactic is run, an agent has already committed to a first move: a goal shape and a family of tactics it expects to use. That choice is usually implicit, buried inside a model call. This component pulls it into the open and answers one question: for a given problem shape, which strategy did the system pick first, and on what visible evidence?

The constraint is what the answer is allowed to depend on. The scorer never sees the oracle's expected strategy, the ground-truth proof, or any provider output. The constraint is what the answer is allowed to depend on. The scorer never sees the oracle's expected strategy, the ground-truth proof, or any provider output. It works from public feature tags and a strategy atlas of trigger features, negative triggers, and retrieval-expansion terms. The selected strategy is a hypothesis recomputed from readable inputs, not a label copied from an answer key.

A loose classifier fails here in two ways. It can bake the answer in by declaring the chosen strategy as a plain label, or it can score on shallow feature overlap that happens to line up with the known-good label. A loose classifier fails here in two ways. It can bake the answer in by declaring the chosen strategy as a plain label, or it can score on shallow feature overlap that happens to line up with the known-good label. This component rejects both. A declared selection must match the score the component recomputes, and a strategy chosen on overlap alone is a typed negative case rather than a pass.

How it works

The entrypoints are run for the fixture and run_strategy_bundle for the exported bundle. Both call _build_result, which runs the stages below in order and then hands the result to write_receipts. The entrypoints are run for the fixture and run_strategy_bundle for the exported bundle. Both call _build_result, which runs the stages below in order and then hands the result to write_receipts.

_build_result loads three public inputs: strategy_atlas.json, problem_features.json, and hypothesis_cases.json. _build_result loads three public inputs: strategy_atlas.json, problem_features.json, and hypothesis_cases.json. It scans every input path for non-public-state leakage first, so a blocking scan hit fails the run before scoring is trusted. Then it runs scoring, the copied-body floor check, and the source-artifact consistency check, and it derives a single status that is PASS only when all of them pass and no expected negative case is missing.

validate_strategy_selection is the scoring core. For each case it calls _score_case, which calls _score_strategy once per candidate. validate_strategy_selection is the scoring core. For each case it calls _score_case, which calls _score_strategy once per candidate. The score is one integer from three terms. Each problem feature that matches a strategy's trigger_features adds four points (TRIGGER_FEATURE_WEIGHT). Each feature that matches its negative_triggers subtracts three (NEGATIVE_TRIGGER_PENALTY). Each retrieval-query term found in the strategy's expansion terms adds one point (RETRIEVAL_TERM_BONUS), capped at two (RETRIEVAL_BONUS_CAP). Plain feature overlap is recorded as a diagnostic count and kept out of the score.

Selection is a deterministic sort. Only strategies with a positive score are eligible. Selection is a deterministic sort. Only strategies with a positive score are eligible. Among those, _score_case ranks by score highest first, breaks ties by the strategy's declared order and then its id, and takes the top row. If no candidate scores positive the case resolves to STRATEGY_SELECTION_MISS. Each case record carries the selected id, the score, the component breakdown, the ranked candidate scores, and the trigger, negative, and retrieval hits that produced them.

The weights encode the design intent. Trigger matches are worth more than retrieval matches, so a strategy is chosen for the shape it claims to handle, not for how many search terms coincide. The weights encode the design intent. Trigger matches are worth more than retrieval matches, so a strategy is chosen for the shape it claims to handle, not for how many search terms coincide. A negative trigger can veto a strategy that looks apt. The retrieval cap stops a strategy from winning on keyword volume.

The same recomputation enforces honesty. When a case declares its own selected_strategy_id, score, classifier, retrieval_bonus, or candidate_scores, _verify_declared_case_outcomes recomputes each from the evidence and reports a stale-declaration finding on any mismatch. The same recomputation enforces honesty. When a case declares its own selected_strategy_id, score, classifier, retrieval_bonus, or candidate_scores, _verify_declared_case_outcomes recomputes each from the evidence and reports a stale-declaration finding on any mismatch. A case that declares only a bare selected_strategy_id, with nothing to check it against, is rejected as label-only.

Two further checks guard the copied inputs. validate_source_module_imports reads source_module_manifest.json and confirms each copied source body against its recorded SHA-256 digest, line count, byte count, and required anchors, and rejects any body that would land inside a generated result record. Two further checks guard the copied inputs. validate_source_module_imports reads source_module_manifest.json and confirms each copied source body against its recorded SHA-256 digest, line count, byte count, and required anchors, and rejects any body that would land inside a generated result record. validate_source_artifact_consistency opens the three copied runtime artifacts (strategy_cards.json, strategy_hypothesis_set.json, prover_skill_atlas.json) and checks them for oracle-label and proof-body leakage. write_receipts then emits four metadata-only result records: mathematical_strategy_atlas_result.json, mathematical_strategy_atlas_board.json, mathematical_strategy_atlas_validation_receipt.json, and a fixture-sign-off record. Each carries refs, counts, hits, and verdicts, never body text.

flowchart TD inputs["strategy_atlas.json problem_features.json hypothesis_cases.json"] scan["scan inputs for non-public-state leakage"] score["_score_strategy trigger x4 - negative x3 + retrieval (cap 2)"] select{"any positive score?"} selected["selected_strategy_id + score breakdown"] miss["STRATEGY_SELECTION_MISS"] verify["recompute vs declared fields"] result records["four metadata-only result records"] inputs --> scan scan --> score score --> select select -- yes --> selected select -- no --> miss selected --> verify miss --> verify verify --> result records

Negative cases

The fixture supplies eight named negative cases in EXPECTED_NEGATIVE_CASES, and the run fails if any expected case is not observed. The fixture supplies eight named negative cases in EXPECTED_NEGATIVE_CASES, and the run fails if any expected case is not observed. unknown_strategy_id rejects a strategy id outside the public enum. proof_body_with_strategy rejects any proof, provider, or source body field on a case. oracle_strategy_label_leakage rejects a fixture that exposes an oracle strategy label. post_oracle_strategy_selection rejects a case marked as selected after oracle labels are visible. release_overclaim rejects a payload that tries to set release_authorized or any sibling authority flag. superficial_overlap_only_scoring rejects legacy unweighted overlap as the decision rule. missing_rich_strategy_card_fields rejects a strategy card that lacks trigger_features, negative_triggers, retrieval_expansion_terms, or proof_plan_template. retrieval_bonus_ceiling_overclaim rejects a claimed retrieval cap above two.

Prior Art Grounding

The atlas follows the formal-methods practice of separating problem-shape classification from proof execution. Lean's tactic model, described in Theorem Proving in Lean 4, is the immediate precedent: proof work is arrange around tactics chosen for a goal shape while the kernel checks the final proof state. The atlas follows the formal-methods practice of separating problem-shape classification from proof execution. Lean's tactic model, described in Theorem Proving in Lean 4, is the immediate precedent: proof work is arrange around tactics chosen for a goal shape while the kernel checks the final proof state. The mathlib overview motivates explicit retrieval terms and domain tags, because a large formal library is navigated by topic and reusable theorem families. The pattern is also adjacent to hammer-style method selection such as Isabelle Sledgehammer, where a front-end tool searches for useful facts before replay. This component keeps the pattern pre-oracle and metadata-only: it records why a first strategy was selected, not whether the proof can be completed.

Validation Result record Path

Run from microcosm-substrate:

PYTHONPATH=src ../repo-python -m microcosm_core.organs.mathematical_strategy_atlas_hypothesis_scorer run \
  --input fixtures/first_wave/mathematical_strategy_atlas_hypothesis_scorer/input \
  --out /tmp/microcosm-mathematical-strategy-atlas-hypothesis-scorer/fixture \
  --card
PYTHONPATH=src ../repo-python -m microcosm_core.organs.mathematical_strategy_atlas_hypothesis_scorer run-strategy-bundle \
  --input examples/mathematical_strategy_atlas_hypothesis_scorer/exported_mathematical_strategy_atlas_bundle \
  --out /tmp/microcosm-mathematical-strategy-atlas-hypothesis-scorer/bundle \
  --card
PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider tests/test_mathematical_strategy_atlas_hypothesis_scorer.py -q
PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

What a green strategy run establishes

A green run means the strategy scoring, the copied-body digests, the source-artifact consistency, and the eight negative cases all checked out. A green run means the strategy scoring, the copied-body digests, the source-artifact consistency, and the eight negative cases all checked out. It does not mean a proof ran.