{"data":{"kind":"file","path":"README.md","version_id":"ckwgynx3rt4smb0e2k46k15h","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":3267,"modified_at":"2026-09-12T09:55:26.626000","content_hash":"8db24a589227e7d33b4d697fc7ac669bfde772e0195c50a842e03c809712d8dd"},"entries":[],"content":"# MathCheck RL\n\nMathCheck RL is an answer-key-free reinforcement-learning and evaluation\nenvironment for bounded integer mathematics. It generates each prompt and its\ntrusted checker from one frozen bounded specification. A model submits an\ninteger candidate or a complete pair certificate in fenced JSON; it does not\nsubmit a Lean proof or replace the specification.\n\nReward is binary. A reward of `1` means the submission satisfied the complete\nencoded bounded specification. Scalar tasks establish the exact bounded\nevaluation, sum, count, or minimum. Pair-certificate tasks establish equality\nwith the entire satisfying relation in the declared rectangle and the claimed\ncardinality. The claim is limited to the encoded bounds; this environment does\nnot claim to prove arbitrary mathematical prose or facts outside those bounds.\n\nThe environment does not store an expected candidate. In the compatibility\nAPI, the framework column named `answer` carries only the frozen checker\nspecification and is never rendered into the model prompt. Train and evaluation\ntasks are generated deterministically and are disjoint by specification digest.\n\n## Task configuration\n\n- `families`: `all` or a comma-separated subset of supported bounded families.\n- `num_per_family`: number of generated training tasks per family.\n- `seed`: deterministic training-generation seed.\n- `eval_num_per_family`: compatibility-API evaluation tasks per family.\n- `eval_seed`: deterministic compatibility-API evaluation seed.\n- `task.verify_timeout`: Verifiers v1 native-check timeout in seconds.\n- `task.lean_bin`: optional explicit path to the isolated Lean launcher.\n\n## Submission format\n\nThe prompt states the exact JSON schema. A scalar task uses a fenced object such\nas:\n\n```json\n{\"answer\": 17}\n```\n\nPair tasks require the complete bounded relation and its cardinality in the\nschema shown by that task. Extra prose, replacement specifications, malformed\nJSON, incomplete relations, duplicates, and out-of-bounds pairs are rejected.\n\n## Reward and metrics\n\n- `nv_specification_pass`: reward `1.0` only for an accepted complete result;\n  otherwise `0.0`.\n- `nv_stage_rank`: zero-weight diagnostic metric for checker progress.\n- Verification status, stage, reason, and specification digest are recorded in\n  trace metadata.\n\nTimeouts and backend failures fail closed with zero reward and an operational\nstatus. They are not reported as mathematical counterexamples.\n\n## Runtime requirements\n\nExecution requires Linux, MathCheck Engine's `lean-isolated` launcher, and a\nstandalone Lean 4.23.0 distribution. Configure:\n\n```bash\nexport NATIVE_VERIFY_LEAN=/absolute/path/to/lean-isolated\nexport LKV_SANDBOX_TOOLCHAIN=/absolute/path/to/lean-4.23.0-linux\n```\n\nThe launcher requires bubblewrap and a kernel that permits its isolation mode.\nMissing isolation fails closed; MathCheck RL does not fall back to executing\nuntrusted model code with an arbitrary host Lean installation.\n\n## Source and scope\n\n- MathCheck RL: https://github.com/stanleyngugi/mathcheck-rl\n- MathCheck Engine: https://github.com/stanleyngugi/mathcheck-engine\n\nThe older finite-observation sequence adapter remains in the repository as a\nlegacy experimental baseline. It is not the contract published by this Hub\nenvironment.\n","encoding":"utf-8","truncated":false,"total_bytes":3267},"status":null}