Mathematical Strategy Atlas Hypothesis Scorer

Picks a first-guess proof strategy from a problem's tags and flags any it cannot map.

Contract

Does Before any proof is attempted, this component looks at a math problem's feature tags and writes down its first-guess strategy (for example, "this looks like an if-and-only-if, so split it both ways"), and flags anything it cannot map as an explicit "no strategy matched" instead of a silent failure. The chosen opening move, why it was chosen, and the cases it could not map are all recorded in machine-readable result records.

Scope limit It only projects pre-oracle strategy-hypothesis and retrieval mechanics; it does not run Lean/Lake, prove theorems, establish domain or formal-result correctness, reveal oracle labels, expose proof bodies, use external model services, tune on test answers, or include launch operations.

Run

Command

PYTHONPATH=src python3 -m microcosm_core.organs.mathematical_strategy_atlas_hypothesis_scorer run --input fixtures/first_wave/mathematical_strategy_atlas_hypothesis_scorer/input --out receipts/first_wave/mathematical_strategy_atlas_hypothesis_scorer

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module

Paper module Mathematical Strategy Atlas

Pre-oracle strategy hypotheses make the first proof-search move inspectable without claiming proof or provider authority.

Read the full write-up

Back to Components index → Reference roster →