{"active_K": 20, "active_epoch_randomness_source": "manual", "active_queue_seed": "lemma-active-queue", "active_seed_mode": "static", "active_selection_seed_sha256": "583f36885ecb9e94ae8c1684d0210483e3054b8f811d3d200087b42322b0e7c1", "active_tempo_seconds": 4320, "frontier_depth": 0, "generated_at": "2026-05-21T06:17:48Z", "registry_sha256": "c0f69a5c9dd0bb189e2095f1b3dcffdc062b62ed676ba538601e4d30c8eebcd8", "registry_task_count": 32, "schema_version": 1, "task_count": 20, "tasks": [{"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 4, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_nat_le_refl : \u2200 n : Nat, n \u2264 n := by\n  sorry", "target_sha256": "b8185b3b051a6f30b37dcbc3deef30e169dc2e99db634071d4b1957387703eef", "task_id": "lemma.generated.nat_le_refl", "task_version": 1, "theorem_name": "generated_nat_le_refl", "title": "Generated Nat le refl", "type_expr": "\u2200 n : Nat, n \u2264 n"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 5, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_nat_lt_succ_self : \u2200 n : Nat, n < Nat.succ n := by\n  sorry", "target_sha256": "58735a2681a668f3b0661a9daf9fbf36f45df80ea57ee524fb3376303c664a6d", "task_id": "lemma.generated.nat_lt_succ_self", "task_version": 1, "theorem_name": "generated_nat_lt_succ_self", "title": "Generated Nat lt successor", "type_expr": "\u2200 n : Nat, n < Nat.succ n"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 6, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_list_append_nil : \u2200 xs : List Nat, xs ++ [] = xs := by\n  sorry", "target_sha256": "4defc7af0660a83a8ffe1bbe3edd2e45687e5ad1cf8ca9ab25daf5fdc482327f", "task_id": "lemma.generated.list_append_nil", "task_version": 1, "theorem_name": "generated_list_append_nil", "title": "Generated List append nil", "type_expr": "\u2200 xs : List Nat, xs ++ [] = xs"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 7, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_bool_not_false : Bool.not false = true := by\n  sorry", "target_sha256": "fe2e5446952dc96a604291c19369aa586893c63e082482edb07144997e21bfe6", "task_id": "lemma.generated.bool_not_false", "task_version": 1, "theorem_name": "generated_bool_not_false", "title": "Generated Bool not false", "type_expr": "Bool.not false = true"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 8, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_nat_add_zero : \u2200 n : Nat, n + 0 = n := by\n  sorry", "target_sha256": "dae79b183518b8a1607cafe68129c302de71a38fd9f3e7d155d88cfac15c3ae5", "task_id": "lemma.generated.nat_add_zero", "task_version": 1, "theorem_name": "generated_nat_add_zero", "title": "Generated Nat add-zero", "type_expr": "\u2200 n : Nat, n + 0 = n"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 9, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_and_left : \u2200 p q : Prop, p \u2227 q \u2192 p := by\n  sorry", "target_sha256": "109467ac80abbf12ed54e2b8bc546b6634c6585423bb4b8fc8d5d00be967a9a0", "task_id": "lemma.generated.and_left", "task_version": 1, "theorem_name": "generated_and_left", "title": "Generated conjunction left", "type_expr": "\u2200 p q : Prop, p \u2227 q \u2192 p"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 10, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_exists_zero : \u2203 n : Nat, n = 0 := by\n  sorry", "target_sha256": "db8d91251f2b69fcad461998aeb84f214a4b7a25bca4f0c5c9718897ad02afe2", "task_id": "lemma.generated.exists_zero", "task_version": 1, "theorem_name": "generated_exists_zero", "title": "Generated exists zero", "type_expr": "\u2203 n : Nat, n = 0"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 11, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_bool_not_true : Bool.not true = false := by\n  sorry", "target_sha256": "36210b417e7069a617edf11db84ecb43bcaa8b272dff6a253d021b74dbfb1d92", "task_id": "lemma.generated.bool_not_true", "task_version": 1, "theorem_name": "generated_bool_not_true", "title": "Generated Bool not true", "type_expr": "Bool.not true = false"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 12, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_true_intro : True := by\n  sorry", "target_sha256": "3df244fb4dc02549062c6febdb5beb648e818ac970a80dc0b887d349761c2437", "task_id": "lemma.generated.true_intro", "task_version": 1, "theorem_name": "generated_true_intro", "title": "Generated True", "type_expr": "True"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 13, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_false_or : \u2200 p : Prop, p \u2192 False \u2228 p := by\n  sorry", "target_sha256": "2883bdeb9a07720df25657aef53d4c3618206bfa2012593b6b1d31ac167aba50", "task_id": "lemma.generated.false_or", "task_version": 1, "theorem_name": "generated_false_or", "title": "Generated left disjunction", "type_expr": "\u2200 p : Prop, p \u2192 False \u2228 p"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 14, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_and_intro : True \u2227 True := by\n  sorry", "target_sha256": "d48ef2ace650deff92beaaa99f7b08e22510c507dc139267ce32da1880a01411", "task_id": "lemma.generated.and_intro", "task_version": 1, "theorem_name": "generated_and_intro", "title": "Generated conjunction", "type_expr": "True \u2227 True"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 15, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_eq_trans_nat : \u2200 a b c : Nat, a = b \u2192 b = c \u2192 a = c := by\n  sorry", "target_sha256": "53788788ccc32c013ab6d4cbb0eedc514dc2c824912f5ba159ad7befcd863e04", "task_id": "lemma.generated.eq_trans_nat", "task_version": 1, "theorem_name": "generated_eq_trans_nat", "title": "Generated Nat equality transitivity", "type_expr": "\u2200 a b c : Nat, a = b \u2192 b = c \u2192 a = c"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 16, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_nat_self_eq : \u2200 n : Nat, n = n := by\n  sorry", "target_sha256": "6c2bddfe83d6c363eaf936591467e7e5169ee1024c9a072c7423508bc510ef38", "task_id": "lemma.generated.nat_self_eq", "task_version": 1, "theorem_name": "generated_nat_self_eq", "title": "Generated Nat reflexivity", "type_expr": "\u2200 n : Nat, n = n"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 17, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_and_right : \u2200 p q : Prop, p \u2227 q \u2192 q := by\n  sorry", "target_sha256": "20a0998891a91a332d16b998f6afa14126f21fe2f7b82518592095d1569a11ea", "task_id": "lemma.generated.and_right", "task_version": 1, "theorem_name": "generated_and_right", "title": "Generated conjunction right", "type_expr": "\u2200 p q : Prop, p \u2227 q \u2192 q"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 18, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_prop_id : \u2200 p : Prop, p \u2192 p := by\n  sorry", "target_sha256": "f0adf55d0223665ffa97a7f214597090e9ac6b1974432a69e23531193535f6b4", "task_id": "lemma.generated.prop_id", "task_version": 1, "theorem_name": "generated_prop_id", "title": "Generated proposition identity", "type_expr": "\u2200 p : Prop, p \u2192 p"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 19, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_nat_zero_ne_succ : \u2200 n : Nat, 0 \u2260 Nat.succ n := by\n  sorry", "target_sha256": "ca450d5925b1303d02d1db62413014f44a51ca5b9103c57d7bc5d299a501ae86", "task_id": "lemma.generated.nat_zero_ne_succ", "task_version": 1, "theorem_name": "generated_nat_zero_ne_succ", "title": "Generated Nat zero not succ", "type_expr": "\u2200 n : Nat, 0 \u2260 Nat.succ n"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 20, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_pair_intro : \u2200 p q : Prop, p \u2192 q \u2192 p \u2227 q := by\n  sorry", "target_sha256": "3bf9fc5c1b22efe89afc8706cda045192bd26cf17efa900a0905456de9685b49", "task_id": "lemma.generated.pair_intro", "task_version": 1, "theorem_name": "generated_pair_intro", "title": "Generated conjunction builder", "type_expr": "\u2200 p q : Prop, p \u2192 q \u2192 p \u2227 q"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 21, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_true_or_false : True \u2228 False := by\n  sorry", "target_sha256": "6295461c998e0ab16c0c8f01b929ffb6f14b0e94a4f92bdc9d6f17b2b03263d0", "task_id": "lemma.generated.true_or_false", "task_version": 1, "theorem_name": "generated_true_or_false", "title": "Generated true or false", "type_expr": "True \u2228 False"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 22, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "deterministic-dev-seed", "path": "tasks/registry.json"}, "source_stream": "generated", "statement": "theorem generated_false_implies : \u2200 p : Prop, False \u2192 p := by\n  sorry", "target_sha256": "908797c912dcfe62c302aaaa54138ad2266a877e7caba9dc7781c093e78dd14d", "task_id": "lemma.generated.false_implies", "task_version": 1, "theorem_name": "generated_false_implies", "title": "Generated false elimination", "type_expr": "\u2200 p : Prop, False \u2192 p"}, {"difficulty_band": "easy", "frontier_depth": 0, "lean_toolchain": "leanprover/lean4:v4.30.0-rc2", "mathlib_rev": "5450b53e5ddc", "policy": "restricted_helpers", "queue_depth": 0, "queue_position": 23, "source_license": "CC-BY-4.0", "source_ref": {"kind": "dev_seed", "name": "lemma-dev-smoke", "path": "tasks/registry.json"}, "source_stream": "human_curated", "statement": "theorem true_intro_sample : True := by\n  sorry", "target_sha256": "9b4bfc3ff8964ed0bb150c9775d9e974b5ce81560c47c33f38f73b0597a670a9", "task_id": "lemma.sample.true_intro", "task_version": 1, "theorem_name": "true_intro_sample", "title": "Smoke-test True", "type_expr": "True"}], "tempo": 411885}