Prototype · v0.1-pitch

Critical-Rationalist Machine

A minimal but real, end-to-end machine that creates certified-novel knowledge by bold conjecture → severe automated criticism → retention of survivors and the reasoned genealogy of failures — not by predicting the human-text distribution.

A frozen LLM is demoted from a terminal objective to a proposal distribution; the primary signal becomes survival under a real Refutation Engine. What sets it apart from RLVR / AlphaProof / Absolute Zero: it conditions the proposer on a structured genealogy of why conjectures failed, and scores them by hard-to-vary-ness — not mere pass/fail or validity.

▶ Open the interactive replay Certified-novel survivors Full report Source ↗
7
certified-novel survivors (seed 0; of 18 conjectures, 3 rounds — real critic; 3-seed mean 6.0±2.2)
0.756
certified-novel / kilo-token
0.58s
total critic time to certify 7 (~32 ms/conjecture; not annualized)

The contribution is the ablations

Significance ablation
clear win  Turning the hard-to-vary significance critic ON drops the trivial/vacuous-survivor rate from 0.34 → 0.00 — it catches the “it compiled / it passed” reward-hack that validity-only optimizers fall for.
Genealogy ablation
reported honestly  At this tiny budget the genealogy treatment does not lead on the headline count (6.0±2.2 vs 7.0±0.8) — the mechanism and the per-compute benchmark are the claim; a larger budget is needed to test whether it compounds.

What you’re looking at

The replay viewer reads a committed, sanitized copy of a real run ledger and renders the loop round-by-round: each conjecture as a card coloured by its refutation class, with significance mini-bars (novelty · breadth · hardness), a certified-novel badge, and — under each survivor — the failed siblings the genealogy explains. No API, no network, no Lean: it’s a faithful replay of what actually ran.

Honest limits: frozen proposer (in-context conditioning only); operational, not formal, novelty; small scale (~18 conjectures). The headline rests on the real sandboxed code-exec critic; the Lean 4 / mathlib critic is wired and compiles but produced 0 survivors at the demo budget. Reproduce locally with make demo.