llm-driven-proof-search

KO | EN

gitlite — search

#openai #database #containers #command-line #json #monitoring #api #dotnet #macos #go

llm-driven-proof-search

(★ 9)

An evidence-preserving operating environment for AI-assisted mathematical research, formalization, decomposition, certificate generation, Lean verification, and publication export.

파일 탐색기

ZIP 다운로드

- - ladder.json
  - README.md
- putnambench_smoke.json
- - Cargo.toml
- - Cargo.toml
- - 0001-lean-sandbox-platform-isolation.md
  - 0002-canonical-vs-episode-local-storage.md
  - 0003-hash-chained-trajectories.md
- - putnambench.md
  - serious_math_ladder.md
- - bounty-board.md
- - certificate-interface.md
- - 2026-07-04-putnambench-first-attempt.md
  - 2026-07-04-v0.3.1-overnight-module-sprint.md
  - 2026-07-05-putnam-genuine-attempt.md
  - 2026-07-06-erdos-corpus-validation.md
  - 2026-07-06-putnam-retry-six.md
  - 2026-07-07-erdos-calibration-audit.md
  - handoff-2026-07-06-putnam-retry-six.md
  - putnambench-gap-infrastructure-after-8-of-12.md
- fix_plan_playtest_01.md
- fix_plan_playtest_02.md
- fix_plan_playtest_03.md
- fix_plan_playtest_04.md
- fix_plan_playtest_05.md
- gitflow_workflow.md
- handoff-reasoning-logs-sop.md
- handoff-scratchpad.md
- igp24_gate.md
- librarian.md
- llm_native_design_practices.md
- mathlib-contribution-no-fermat-sub.md
- roadmap.md
- sop-reasoning-logs.md
- submit_module.md
- tdd_requirements.md
- - .gitignore
  - agent_alt_search_t167_periodic.rs
  - agent_alt_search_tt56_dualmargin.rs
  - agent_alt_t167_periodic_live.json
  - agent_alt_t167_periodic_summary.json
  - agent_alt_tt56_dualmargin_live.json
  - agent_alt_tt56_dualmargin_summary.json
  - agent_bgpu_parity_classes.py
  - agent_bgpu_psd_cap.py
  - agent_bgpu_psd_run1_class_00_live.json
  - agent_bgpu_psd_run1_class_01_live.json
  - agent_bgpu_psd_run1_class_02_live.json
  - agent_bgpu_psd_run1_class_03_live.json
  - agent_bgpu_psd_run1_class_05_live.json
  - agent_bgpu_psd_run1_class_07_live.json
  - agent_bgpu_psd_run1_class_08_live.json
  - agent_bgpu_psd_run1_class_11_live.json
  - agent_bgpu_psd_run1_classes_summary.json
  - agent_bgpu_psd_run1_live.json
  - agent_bgpu_psd_run1_summary.json
  - agent_bgpu_psd_smoke_class_00_live.json
  - agent_bgpu_psd_smoke_class_01_live.json
  - agent_bgpu_psd_smoke_class_02_live.json
  - agent_bgpu_psd_smoke_class_03_live.json
  - agent_bgpu_psd_smoke_class_05_live.json
  - agent_bgpu_psd_smoke_class_07_live.json
  - agent_bgpu_psd_smoke_class_08_live.json
  - agent_bgpu_psd_smoke_class_11_live.json
  - agent_bgpu_psd_smoke_classes_summary.json
  - agent_bgpu_psd_smoke_live.json
  - agent_bgpu_psd_smoke_summary.json
  - agent_bgpu_run1_fourier_class_00_live.json
  - agent_bgpu_run1_fourier_class_01_live.json
  - agent_bgpu_run1_fourier_class_02_live.json
  - agent_bgpu_run1_fourier_class_03_live.json
  - agent_bgpu_run1_fourier_class_04_live.json
  - agent_bgpu_run1_fourier_class_05_live.json
  - agent_bgpu_run1_fourier_class_06_live.json
  - agent_bgpu_run1_fourier_class_07_live.json
  - agent_bgpu_run1_fourier_class_08_live.json
  - agent_bgpu_run1_fourier_class_09_live.json
  - agent_bgpu_run1_fourier_class_10_live.json
  - agent_bgpu_run1_fourier_class_11_live.json
  - agent_bgpu_run1_fourier_classes_live.json
  - agent_bgpu_run1_fourier_classes_summary.json
  - agent_bgpu_run1_fourier_live.json
  - agent_bgpu_run1_fourier_summary.json
  - agent_bgpu_run1_parity_live.json
  - agent_bgpu_run1_parity_summary.json
  - agent_bgpu_smoke_fourier_class_02_live.json
  - agent_bgpu_smoke_fourier_class_03_live.json
  - agent_bgpu_smoke_fourier_class_04_live.json
  - agent_bgpu_smoke_fourier_class_07_live.json
  - agent_bgpu_smoke_fourier_class_08_live.json
  - agent_bgpu_smoke_fourier_class_11_live.json
  - agent_bgpu_smoke_fourier_classes_live.json
  - agent_bgpu_smoke_fourier_classes_summary.json
  - agent_bgpu_smoke_fourier_live.json
  - agent_bgpu_smoke_fourier_summary.json
  - agent_bgpu_smoke_parity_live.json
  - agent_bgpu_smoke_parity_summary.json
  - agent_bp2_e736_verified.json
  - agent_bp2_e832_verified.json
  - agent_bp2_enumerate_equal_margins.py
  - agent_bp2_fourier_e1056_verified.json
  - agent_bp2_fourier_e1216_verified.json
  - agent_bp2_fourier_e896_verified.json
  - agent_bp2_fourier_exact_summary.json
  - agent_bp2_fourier_live.json
  - agent_bp2_fourier_summary.json
  - agent_bp2_gf2_spectral_shells.py
  - agent_bp2_gf2_spectral_shells_summary.json
  - agent_bp2_nearest_margins.py
  - agent_bp2_o7r12_cap.py
  - agent_bp2_order11_nearest.py
  - agent_bp2_parity_memetic.rs
  - agent_bp2_rank_margin_pairs.py
  - agent_bp2_rank_o7_radius12.py
  - agent_bp2_ranked_c8q8.json
  - agent_bp2_ranked_o7_radius12.json
  - agent_bp2_scan2_best.json
  - agent_bp2_scan2_e736_best.json
  - agent_bp2_scan2_e736_guided.json
  - agent_bp2_scan2_fourier_exact.json
  - agent_bp2_scan2_guided.json
  - agent_bp2_spectral_e2144_verified.json
  - agent_bp2_spectral_e2784_verified.json
  - agent_bp2_spectral_e2976_verified.json
  - agent_bp2_spectral_projection.py
  - agent_bp2_spectral_projection_e2784_o7flex8.json
  - agent_bp2_spectral_projection_e896.json
  - agent_bp2_summary.json
  - agent_bs_crossfiber.rs
  - agent_bs_crossfiber_live.json
  - agent_bs_crossfiber_summary.json
  - agent_bs_signature_cpsat.py
  - agent_bs_signature_cpsat_summary.json
  - agent_bsd_crossover_e552_to_e896.json
  - agent_bsd_crossover_grouped.py
  - agent_bsd_crossover_grouped_e552_to_e896.json
  - agent_bsd_cycle_tabu.rs
  - agent_bsd_dual_tabu.rs
  - agent_bsd_e896_cycle_summary.json
  - agent_bsd_e896_pair_summary.json
  - agent_bsd_e896_quad_summary.json
  - agent_bsd_e896_quad_tabu_summary.json
  - agent_bsd_e896_triple_summary.json
  - agent_bsd_gf2_batch.json
  - agent_bsd_gf2_batch.py
  - agent_bsd_gf2_compatibility.json
  - agent_bsd_gf2_compatibility.py
  - agent_bsd_live.json
  - agent_bsd_pair_scan.rs
  - agent_bsd_pair_summary.json
  - agent_bsd_parity0_live.json
  - agent_bsd_parity0_summary.json
  - agent_bsd_parity_repair.py
  - agent_bsd_parity_repair_grouped.py
  - agent_bsd_parity_repair_milp.py
  - agent_bsd_parity_repair_sat.py
  - agent_bsd_parity_repair_z3.py
  - agent_bsd_parityguide_summary.json
  - agent_bsd_plus2_compatibility.json
  - agent_bsd_plus2_pair_live.json
  - agent_bsd_plus2_pair_summary.json
  - agent_bsd_plus2_parity0_live.json
  - agent_bsd_plus2_parity0_summary.json
  - agent_bsd_quad_scan.rs
  - agent_bsd_recovered_576.json
  - agent_bsd_repair_grouped_plus2_pb0.json
  - agent_bsd_soft2_live.json
  - agent_bsd_soft2_summary.json
  - agent_bsd_soft3_live.json
  - agent_bsd_soft3_summary.json
  - agent_bsd_soft4_live.json
  - agent_bsd_soft4_summary.json
  - agent_bsd_soft5_live.json
  - agent_bsd_soft5_summary.json
  - agent_bsd_soft6_live.json
  - agent_bsd_soft6_summary.json
  - agent_bsd_soft_live.json
  - agent_bsd_soft_pb10_live.json
  - agent_bsd_soft_pb12_live.json
  - agent_bsd_soft_pb14_live.json
  - agent_bsd_soft_pb4_live.json
  - agent_bsd_soft_pb6_live.json
  - agent_bsd_soft_pb8_live.json
  - agent_bsd_soft_summary.json
  - agent_bsd_summary.json
  - agent_bsd_triple_scan.rs
  - agent_bsd_unrestricted_live.json
  - agent_bsd_unrestricted_summary.json
  - agent_btt_e800_shell_summary.json
  - agent_btt_e800_verified.json
  - agent_btt_exact_tabu.rs
  - agent_btt_fourier_compatibility.json
  - agent_btt_fourier_compatibility.py
  - agent_btt_minicard.py
  - agent_btt_parity_project.py
  - agent_btt_parity_projection_t0.json
  - agent_btt_parity_projection_t0_feasible.json
  - agent_btt_spectral_targets.json
  - agent_btt_spectral_targets.py
  - agent_btt_t0_feasible_exact_live.json
  - agent_btt_t0_feasible_exact_summary.json
  - agent_btt_t0_h16_exact_live.json
  - agent_btt_t0_h16_exact_summary.json
  - agent_gs_crossrow_mitm.py
  - agent_gs_crossrow_summary.json
  - agent_gs_fourpart_coordinate.py
  - agent_gs_fourpart_summary.json
  - agent_gspec_21_11_9_5_gpu_live.json
  - agent_gspec_21_11_9_5_gpu_summary.json
  - agent_gspec_21_11_9_5_seed.json
  - agent_gspec_21_13_7_3_gpu_live.json
  - agent_gspec_21_13_7_3_gpu_summary.json
  - agent_gspec_21_13_7_3_seed.json
  - agent_gspec_altproj960_summary.json
  - agent_gspec_altproj_gpu.py
  - agent_gspec_campaign_summary.md
  - agent_gspec_coevolve960_summary.json
  - agent_gspec_coevolve_gpu.py
  - agent_gspec_coevolve_paley_summary.json
  - agent_gspec_coevolve_two_paley_live.json
  - agent_gspec_coevolve_two_paley_summary.json
  - agent_gspec_lns_summary.json
  - agent_gspec_make_two_paley.py
  - agent_gspec_pair_altproj_gpu.py
  - agent_gspec_pair_altproj_summary.json
  - agent_gspec_pair_hardcap_gpu.py
  - agent_gspec_pair_hardcap_live.json
  - agent_gspec_pair_hardcap_multi_gpu.py
  - agent_gspec_pair_hardcap_multi_summary.json
  - agent_gspec_pair_hardcap_summary.json
  - agent_gspec_pair_hardcap_topmoves.py
  - agent_gspec_pair_hardcap_topmoves_summary.json
  - agent_gspec_pair_psd_feasible_live.json
  - agent_gspec_pair_psd_gpu.py
  - agent_gspec_pair_psd_summary.json
  - agent_gspec_paley_minicard.py
  - agent_gspec_two_paley_from_hardcap_gpu_live.json
  - agent_gspec_two_paley_from_hardcap_gpu_summary.json
  - agent_gspec_two_paley_gpu_live.json
  - agent_gspec_two_paley_gpu_summary.json
  - agent_gspec_two_paley_minicard.py
  - agent_gspec_two_paley_reduction.md
  - agent_gspec_two_paley_seed.json
  - agent_gspec_two_paley_symmetric_gpu.py
  - agent_gspec_two_paley_symmetric_gpu_live.json
  - agent_gspec_two_paley_symmetric_gpu_summary.json
  - agent_gspec_two_paley_symmetric_minicard.py
  - agent_gspec_weighted960_summary.json
  - agent_gspec_weighted_gpu.py
  - anneal_lp333_271_orbitspace.py
  - bs_84_83_alt_live.json
  - bs_84_83_alt_parity_summary.json
  - bs_84_83_bsd576_parity_projection.json
  - bs_84_83_cpsat_10_8_m1_m13_best.json
  - bs_84_83_cpsat_10_8_m1_m13_long_best.json
  - bs_84_83_from142_row_parity_projection.json
  - bs_84_83_live.json
  - bs_84_83_row568_parity_projection.json
  - bs_84_83_row_parity_summary.json
  - bs_84_83_row_rank_live.json
  - bs_84_83_row_summary.json
  - bs_84_83_soft552_parity_row_alt_projection.json
  - bs_84_83_soft552_parity_row_projection.json
  - bs_84_83_summary.json
  - bs_84_83_tabu_live.json
  - build_hadamard_668.py
  - build_hadamard_668_from_pair.py
  - compression3_order6_fibers.py
  - compression9_z37_layer.py
  - convert_gs_checkpoint.py
  - enum_lp333_subgroups.py
  - exhaustive_271_compression3.py
  - exhaustive_group333_fiber.py
  - exhaustive_group333_v2.py
  - external_Hadamard_Proof
  - g_matrices_167_summary.json
  - generate_legendre37_character.py
  - good_167_live.json
  - good_167_summary.json
  - good_product_167_live.json
  - good_product_167_summary.json
  - gpu_layerB_kb6.py
  - gpu_lift_196.jsonl
  - gpu_lift_307.jsonl
  - gpu_lift_group333.jsonl
  - gpu_lift_group333_eigen.py
  - gpu_lift_order6_exhaust.py
  - gpu_z37_order3_stream.py
  - gpu_z37_order3_v2.py
  - group333_eigen_surviving_classes.npy
  - group333_exhaustive_queue.json
  - group333_kb6_layerB.jsonl
  - group333_tail_layer_verdicts.jsonl
  - gs_167_17_17_9_3_seed.json
  - gs_167_23_11_3_3_seed.json
  - gs_167_23_9_7_3_gpu_summary.json
  - gs_167_23_9_7_3_seed.json
  - gs_167_23_9_7_3_topmoves_live.json
  - gs_167_23_9_7_3_topmoves_summary.json
  - gs_167_25_5_3_3_seed.json
  - gs_167_best960_ring.json
  - gs_167_best960_ring_cpsat.py
  - gs_167_best960_ring_sqcap_K10_4608_final.json
  - gs_167_best960_ring_sqcap_K4_3456_final.json
  - gs_167_best960_ring_sqcap_K6_4928_final.json
  - gs_167_best960_ring_sqcap_K8_4608_final.json
  - gs_167_best960_ring_tier1.lp
  - gs_167_best960_ring_tier1.opb
  - gs_167_best960_ring_tier2.lp
  - gs_167_best960_ring_tier2.opb
  - gs_167_best960_ring_tier3.lp
  - gs_167_best960_ring_tier3.opb
  - gs_167_cpsat_l1_r100.json
  - gs_167_cpsat_l1_r120_from960.json
  - gs_167_cross_960_1056_summary.json
  - gs_167_cross_960_1120_summary.json
  - gs_167_gpu30m_summary.json
  - gs_167_gpu_anneal960_lowtemp_summary.json
  - gs_167_gpu_anneal960_summary.json
  - gs_167_gpu_anneal_17_17_9_3_summary.json
  - gs_167_gpu_anneal_23_11_3_3_summary.json
  - gs_167_gpu_anneal_smoke_summary.json
  - gs_167_gpu_from960_summary.json
  - gs_167_gpu_relax960_summary.json
  - gs_167_gpu_relax_smoke_summary.json
  - gs_167_gpu_smoke_summary.json
  - gs_167_native_15_15_13_7_live.json
  - gs_167_native_15_15_13_7_summary.json
  - gs_167_native_17_17_9_3_live.json
  - gs_167_native_17_17_9_3_summary.json
  - gs_167_native_19_15_9_1_live.json
  - gs_167_native_19_15_9_1_summary.json
  - gs_167_native_21_15_1_1_live.json
  - gs_167_native_21_15_1_1_summary.json
  - gs_167_native_23_11_3_3_live.json
  - gs_167_native_23_11_3_3_summary.json
  - gs_167_native_23_9_7_3_live.json
  - gs_167_native_23_9_7_3_summary.json
  - gs_167_native_25_5_3_3_live.json
  - gs_167_native_25_5_3_3_summary.json
  - gs_167_native_live.json
  - gs_167_native_summary.json
  - gs_167_paley_21_15_1_gpu1216_summary.json
  - gs_167_paley_21_15_1_gpu_summary.json
  - gs_167_paley_21_15_1_seed.json
  - gs_167_paley_21_15_1_topmoves_summary.json
  - gs_167_paley_gpu_summary.json
  - gs_167_paley_seed.json
  - gs_167_paley_topmoves_summary.json
  - gs_167_search_summary.json
  - gs_167_tabu_19_17_3_3_live.json
  - gs_167_tabu_19_17_3_3_summary.json
  - gs_167_tabu_best960.json
  - gs_167_tabu_best960_external.json
  - gs_167_tabu_best960_external_repair.json
  - gs_167_topmoves960_summary.json
  - legendre37_character_candidate.json
  - legendre37_live.json
  - legendre37_summary.json
  - legendre9_candidates.json
  - legendre9_native_candidate.json
  - legendre9_native_live.json
  - legendre9_portfolio_1.json
  - legendre9_portfolio_2.json
  - legendre9_portfolio_3.json
  - legendre9_portfolio_4.json
  - legendre9_portfolio_5.json
  - legendre9_portfolio_6.json
  - legendre9_portfolio_7.json
  - legendre9_portfolio_8.json
  - lift_286.jsonl
  - lift_307.jsonl
  - lift_307_probe.jsonl
  - lift_order6_profiles.py
  - lp333_271_split.jsonl
  - lp333_271_split_retry.jsonl
  - lp333_271_z3.jsonl
  - lp333_affine_sweep.jsonl
  - lp333_cpsat_dual_p7_l1_r100.json
  - lp333_crossover_p7_screen_summary.json
  - lp333_crossover_p7_summary.json
  - lp333_crossover_row_p7_summary.json
  - lp333_decimation_sweep.jsonl
  - lp333_dual_from_row6496.json
  - lp333_dual_gpu_best16_summary.json
  - lp333_dual_gpu_p7_summary.json
  - lp333_dual_gpu_seeded_summary.json
  - lp333_dual_gpu_smoke_live.json
  - lp333_dual_gpu_smoke_summary.json
  - lp333_dual_live.json
  - lp333_dual_p2_live.json
  - lp333_dual_p3_live.json
  - lp333_dual_p4_live.json
  - lp333_dual_p7_cpseed_live.json
  - lp333_dual_p7_cycle_smoke_summary.json
  - lp333_dual_p7_cycle_summary.json
  - lp333_dual_p7_live.json
  - lp333_dual_p7b_summary.json
  - lp333_dual_screen_p5_live.json
  - lp333_dual_screen_p5_summary.json
  - lp333_dual_screen_p6_live.json
  - lp333_dual_screen_p6_summary.json
  - lp333_dual_screen_p7_live.json
  - lp333_dual_screen_p7_summary.json
  - lp333_dual_screen_p8_live.json
  - lp333_dual_screen_p8_summary.json
  - lp333_dual_seed.json
  - lp333_dual_seed.txt
  - lp333_dual_summary.json
  - lp333_full_multiplier_sweep.jsonl
  - lp333_group333_exhaustive.jsonl
  - lp333_group333_sweep.jsonl
  - lp333_native_live.json
  - lp333_native_rotate5_summary.json
  - lp333_native_rotate_smoke.json
  - lp333_native_summary.json
  - lp333_order6_compression3.jsonl
  - lp333_order6_z37_layer.jsonl
  - lp333_row_gpu_pairs_summary.json
  - lp333_row_gpu_quads_summary.json
  - lp333_row_gpu_tabu_smoke_summary.json
  - lp333_row_gpu_triples_summary.json
  - lp333_subgroup_lattice.txt
  - make_gs_paley_seed.py
  - make_gs_seed.py
  - middle_layer_class_reps.npy
  - middle_layer_survivors_order6.npz
  - ngp334_multiplier_sweep.jsonl
  - pb_bdd_encoder.py
  - project_bs_parity_cpsat.py
  - project_lp333_dual.py
  - propus_167_11_3_23_live.json
  - propus_167_11_3_23_summary.json
  - propus_167_15_1_21_live.json
  - propus_167_3_17_9_live.json
  - propus_167_3_17_9_summary.json
  - propus_167_5_3_25_live.json
  - propus_167_5_3_25_summary.json
  - propus_167_7_15_13_live.json
  - propus_167_7_15_13_summary.json
  - propus_167_live.json
  - propus_167_summary.json
  - recover_bs_json_from_process.py
  - recover_bs_lists_from_process.py
  - RESULTS.md
  - retry_lp333_271_unknowns.py
  - search_bs_84_83_cpsat.py
  - search_bs_84_83_lns_cpsat.py
  - search_bs_84_83_minicard.py
  - search_bs_84_83_parity.rs
  - search_bs_84_83_tabu.rs
  - search_bs_84_83_torch.py
  - search_good_167.rs
  - search_good_product_167.rs
  - search_gs_167.js
  - search_gs_167_cpsat.py
  - search_gs_167_crossover_gpu.py
  - search_gs_167_gpu_anneal.py
  - search_gs_167_gpu_batched.py
  - search_gs_167_gpu_relax.py
  - search_gs_167_lns_cpsat.py
  - search_gs_167_minicard.py
  - search_gs_167_native.rs
  - search_gs_167_tabu.rs
  - search_gs_167_topmoves_gpu.py
  - search_legendre37.rs
  - search_legendre37_cpsat.py
  - search_legendre9_cpsat.py
  - search_legendre9_native.rs
  - search_lp333_271_deepsplit.py
  - search_lp333_271_fiber_sat.py
  - search_lp333_271_kissat.py
  - search_lp333_271_split.py
  - search_lp333_271_z3.py
  - search_lp333_affine_sweep.py
  - search_lp333_cpsat.py
  - search_lp333_crossover_gpu.py
  - search_lp333_decimation_sweep.py
  - search_lp333_dual.rs
  - search_lp333_dual_gpu.py
  - search_lp333_full_multiplier_sweep.py
  - search_lp333_group333_sweep.py
  - search_lp333_minicard.py
  - search_lp333_multiplier_cpsat.py
  - search_lp333_native.rs
  - search_lp333_row_gpu_tabu.py
  - search_ngp334_multiplier.py
  - search_propus_167.rs
  - search_propus_167_lns_cpsat.py
  - search_special_golay_167.rs
  - search_special_golay_167_cpsat.py
  - search_special_golay_167_cpsat_opt.py
  - search_special_golay_167_cpsat_reduced.py
  - search_special_golay_167_genetic.py
  - search_special_golay_167_pysat_reduced.py
  - search_special_golay_167_torch.py
  - search_special_golay_167_variable_q.rs
  - search_special_golay_167_z3.py
  - search_special_golay_167_z3_reduced.py
  - search_tt56_native.rs
  - search_tt56_pysat.py
  - search_tt56_z3.py
  - search_turyn_type_56.js
  - search_williamson_167.rs
  - special_golay_167_cpsat_opt_live.json
  - special_golay_167_cpsat_opt_summary.json
  - special_golay_167_live.json
  - special_golay_167_native_summary.json
  - special_golay_167_variable_q_live.json
  - special_golay_167_variable_q_rank_live.json
  - special_golay_167_variable_q_rank_summary.json
  - special_golay_167_variable_q_summary.json
  - tt56_live.json
  - tt56_native_summary.json
  - turyn_type_56_search_summary.json
  - williamson_167_live.json
  - williamson_167_row_summary.json
  - williamson_167_summary.json
- generate_hadamard_428.js
- hadamard_428.csv
- hadamard_428_proofsearch.md
- - credit.md
  - evidence.md
  - whitepaper.md
- - attack-plan.md
  - credit.md
  - evidence.md
  - proof-narrative.md
  - whitepaper.md
- - credit.md
  - evidence.md
  - whitepaper.md
- - credit.md
  - evidence.md
  - whitepaper.md
- - alpha-gt-two-proof-sketch.md
  - attack-plan.md
  - credit.md
  - evidence.md
  - whitepaper.md
- - credit.md
  - evidence.md
  - whitepaper.md
- - credit.md
  - Erods Problem Page.png
  - evidence.md
  - Przemek Chojecki's Benchmark Erdos Problem.com.png
  - whitepaper.md
- - credit.md
  - evidence.md
  - whitepaper.md
- - attack-plan.md
  - credit.md
  - evidence.md
  - README.md
  - THEOREM-CATALOG.md
  - whitepaper.md
- - attack-plan.md
- - attack-plan.md
  - credit.md
  - evidence.md
  - README.md
  - THEOREM-CATALOG.md
  - whitepaper.md
- - attack-plan.md
  - checkpoint.md
  - erdos888.pdf
  - evidence.md
  - README.md
- - attack-plan.md
- - bounty-board.md
  - corpus-validation.md
  - disclosure-note.md
  - run-575f57b1-summary.md
- README.md
- whitepaper.md
- - LemmaF2_ridge_optimal_tuning.dossier.md
  - LemmaF2_ridge_optimal_tuning.lean
- igp24_candidates_example.csv
- - attack-plan.md
  - credit.md
  - evidence.md
  - problem.md
  - README.md
  - solution.md
  - THEOREM-CATALOG.md
  - whitepaper.md
- - problem.md
- - problem.md
- - problem.md
- - problem.md
- - problem.md
- README.md
- - 11var_cubic_reduction_gist.py
  - cubic_homogeneous_23_lift.py
  - layered_certificate_11var.py
- Challenge.lean
- ChallengeSolved.lean
- CollateralDamage.lean
- proof-construction.md
- README.md
- whitepaper.md
- - Basic.lean
  - CycleDecomposition.lean
  - Multigraph.lean
  - NoFermatSub.lean
- .gitignore
- lake-manifest.json
- lakefile.toml
- lean-toolchain
- LeanChecker.lean
- README.md
- - README.md
- - close-agents.ps1
  - launch-agents.ps1
- igp24_enrich_targets.py
- igp24_gate.py
- igp24_generate_batch.py
- igp24_generate_lift_probes.py
- igp24_generate_quadratic_lifts.py
- igp24_magma_verify.py
- igp24_poll.py
- igp24_source_cyclotomic_period.py
- igp24_source_lmfdb.py
- igp24_source_m24_muller.py
- igp24_submit.py
- igp24_targets.py
- CLAUDE.md
- README.md
.gitignore
Cargo.lock
Cargo.toml
CLAUDE.md
elan-init.ps1
PatrickTanyaJose.lean
PROOFSEARCH_SPEC.md
PROOFSEARCH_SPEC_DEPRECATED.md
README.md
restore-database.bat
SPEC.md

# CDN으로 사용하기

jsDelivr

jsDelivr는 공개 GitHub 리포지토리를 별도 설정 없이 CDN으로 즉시 서빙합니다. 버전과 파일을 고르면 웹페이지에 바로 붙일 수 있는 링크와 예시 코드가 만들어집니다.

버전

파일

링크

예시

# 프로젝트 배지

Rust 바로가기
MCP 바로가기
License: MIT 바로가기

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

This is a **synthetic reinforcement learning environment** where an external LLM agent attempts to prove mathematical theorems verified by the [Lean 4](https://lean-lang.org/) kernel. It exposes a [Model Context Protocol (MCP)](https://modelcontextprotocol.io/) server so that any MCP-compatible host — Claude Desktop, Cline, Roo Code, a custom Python script, or a distributed training loop — can drive proof search episodes without this environment ever containing a single line of inference code.

## Architecture

```
┌─────────────────────────────────────────────────────────────────┐
│                     External Agent Host                         │
│  (Claude Desktop, Cline, Python RL loop, human, ...)            │
│                                                                 │
│  Chooses model · formats prompt · calls LLM · parses response   │
└────────────────────────┬────────────────────────────────────────┘
                         │  MCP (stdio, JSON-RPC 2.0)
                         │  Protocol version 2025-11-25
                         ▼
┌─────────────────────────────────────────────────────────────────┐
│                     proofsearch-mcp (MCP Server)                     │
│                                                                 │
│  86 tools · typed schemas · JSON Schema 2020-12                 │
└────────────────────────┬────────────────────────────────────────┘
                         │
                         ▼
┌─────────────────────────────────────────────────────────────────┐
│                     proofsearch-core (Engine)                         │
│                                                                 │
│  Episode lifecycle · obligation scheduler · crash recovery       │
│  Atomic step (CAS) · hash-chained trajectories · replay         │
│  Budget leases · reward calculation · dataset export             │
└────────────────────────┬────────────────────────────────────────┘
                         │
                         ▼
┌─────────────────────────────────────────────────────────────────┐
│                     Lean 4 Kernel (Verifier)                    │
│                                                                 │
│  Sandboxed per-attempt · deterministic · timeout-guarded        │
│  Kernel pass / fail is ground truth                             │
└─────────────────────────────────────────────────────────────────┘
```

**Key invariant:** LLM-Driven Proof Search Environment contains **no provider SDKs, no API keys, no model routing, no inference calls, no streaming logic, and no provider retry code.** The external host owns all of that. LLM-Driven Proof Search Environment is the environment; the host is the policy.

As of v0.3.x, LLM-Driven Proof Search Environment verifies more than single theorem bodies — see
[`Solve` vs. `SubmitModule`](#solve-vs-submitmodule) below and
[`docs/submit_module.md`](docs/submit_module.md) for the small local Lean
development this environment now supports (helper defs/theorems, mutual
recursion, staged all-or-nothing verification). For what this represents in
terms of overall system capability and what's still ahead, see
[`docs/roadmap.md`](docs/roadmap.md).

## MCP Tools

**Call `readme_first` before creating any episode.** It's the dedicated
first-contact tool (issue #35): the required proof-search loop, the trust
boundary (tracked MCP actions and Lean verdicts are evidence — your own
reasoning is not), when to use `Solve` vs `SubmitModule`, why a proof check
outside `episode_step` doesn't count as a valid attempt, and the cost/
benchmark-mode boundary. Any agent host — Claude Code, Codex, Kilo Code,
Antigravity, or a custom script — should call this first.

| Tool | Description |
|---|---|
| `readme_first` | Call this first. The proof-search protocol: the loop, trust boundary, mandatory reasoning-log SOP, Solve/SubmitModule guidance, untracked-attempt warning, cost and benchmark-mode boundary |
| `environment_describe` | Protocol version, capabilities, tool schemas, Lean gateway readiness |
| `problem_create` | Register a new problem version (source text + root formal statement). `fidelity_status` starts `unreviewed` |
| `problem_submit_fidelity_review` | Record an evidence-backed determination that a problem's formal statement represents its source text. The ONLY path to `fidelity_status='verified'` — required for `outcome='certified'` |
| `problem_record_benchmark_alignment` | Record a `formal_benchmark_hash_alignment` basis (issue #43): the server verifies the problem hash-matches a registered trusted-benchmark target and sets `fidelity_status='benchmark_aligned'`, unlocking proving without `unsafe_dev_attestation`. Hash alignment, **not** NL review — reaches `kernel_verified` but never `certified` |
| `problem_list` | List known problem versions (includes the hashes a reviewer must submit back unchanged) |
| `episode_create` | Start an episode from a problem version with `fidelity_status` `verified` or `attested` |
| `episode_reset` | Nondestructive reset — creates a new episode with `parent_episode_id` |
| `episode_observe` | Get the current observation and pending action request |
| `attempt_claim` | Claim a pending action request to obtain the `action_attempt_id` + `claim_token` required by `episode_step` |
| `episode_step` | Submit a typed action (`Solve` / `SubmitModule` / `Decompose` / `GiveUp`) with CAS revision check. Hard-gated by the fresh-log cadence in [the reasoning-log SOP](docs/sop-reasoning-logs.md) |
| `reasoning_log` | Add or observe SOP-mandated, append-only problem-solving checkpoints. Ordinary work gets at most two `episode_step` submissions between logs; `GiveUp` always requires a fresh log with detailed actual outcome and lesson fields. Process metadata only, never proof |
| `episode_status` | Episode state, revision, budget, step count, outcome |
| `episode_close` | Gracefully terminate an active episode |
| `model_call_reserve` | Reserve a budget lease before calling an external model |
| `model_call_settle` | Settle or void a lease (provider failure, cancellation) |
| `trajectory_export` | Paginated export of hash-chained trajectory events |
| `episode_replay` | Re-execute typed actions (`Solve` or `SubmitModule`) through Lean and verify trajectory integrity |
| `proof_export` | Proof dossier in one of 7 modes: `markdown` (default), `lean`, `public_summary` (redacted, never includes the proof body), `audit_archive`, `training_export` (structured JSON for SFT/RL/DPO), `paper_dossier` (adds a written narrative), `maintainer_submission`. Modes exposing the proof body require `allow_putnambench_proof_export=true` when the episode is linked to a tracked benchmark suite — see [docs/benchmarks/putnambench.md](docs/benchmarks/putnambench.md) |
| `lean_declaration_lookup` | Checks whether names resolve under a problem's import manifest (fast, default). Pass `deep_check=true` to also check under the full Mathlib umbrella and distinguish "not imported here" from "genuinely absent" (slow — loads all of Mathlib). Call this before concluding an API is unavailable |
| `proof_pattern` | ONE tool for the proof-pattern-library family (issue #24 proof-pattern memory), dispatching on an internally-tagged `action` (`create` / `search` / `record_application`) — exactly like `episode_step`'s typed `action`. The pattern library is **purely advisory**: no action here can ever mark anything proved or change fidelity/certification status. `create` registers a reusable proof-pattern lesson (failure signature + recommended repair), rejecting a duplicate `pattern_key` rather than overwriting it; `search` free-text searches the library, or lists it whole — call before repeating a failure another attempt already diagnosed; `record_application` records that a pattern was relevant to a real episode/attempt (failed example, repair example, or suggested hint) — insert-only metadata that never touches proof/fidelity/certification status. `distilled_strategy_add` is dossier-scoped, not pattern-library-scoped, and remains its own tool below rather than folding into this one |
| `draft` | ONE tool for the draft artifact lifecycle (issue #23), dispatching on an internally-tagged `action` (`create` / `observe` / `extract_moves`) — exactly like `episode_step`'s typed `action`. `create` registers an informal Draft artifact — untrusted planning/reasoning content preserved before formalization begins; a draft can **never** mark anything proved; `observe` reads back a draft's content and any moves recorded against it; `extract_moves` records structured moves (construction, auxiliary_lemma, case_split, induction, reduction, bijection, counterexample_search, asymptotic_step, external_citation, unknown) the external agent identified in a draft — metadata only, moves are not obligations until explicitly promoted into a formalization plan item |
| `formalization_plan` | ONE tool for the whole Level 3 formalization-plan family, dispatching on an internally-tagged `action` (`create` / `observe` / `update` / `add_item` / `attach_lookup` / `promote_item_to_obligation` / `attach_librarian_result`) — exactly like `episode_step`'s typed `action`. Advisory scaffolding, never proof authority: `promote_item_to_obligation` links a plan item to an episode_obligation that **already exists** (created via a normal `Decompose` action) and never creates one; `attach_lookup` / `attach_librarian_result` attach `lean_declaration_lookup` / Mathlib-librarian search results to a plan item as hints, updating its Mathlib coverage status but never proof status |
| `research_dossier` | ONE tool for the whole Level 4 research-dossier family, dispatching on an internally-tagged `action` (`create` / `observe` / `node_add` / `external_reference_add` / `assumption_boundary_add` / `citation_review_add` / `verification_layer_set`) — exactly like `episode_step`'s typed `action`. Explicit trust-boundary metadata, never proof authority: `external_reference_add` records citations as **tracked assumptions**, never proof; `citation_review_add` records human review, which remains distinct from Lean verification; `verification_layer_set` is the **only path** to a `kernel_verified` layer and accepts that status only where kernel evidence already exists (e.g. a node whose `trust_status` is already `proved_in_episode`, backed by a verified lemma from **this dossier's own** episode/problem context) |
| `candidate_construction` | ONE tool for the whole candidate-construction family (issue #8), dispatching on an internally-tagged `action` (`add` / `observe` / `update_status` / `link_node` / `link_verification_layer`) — exactly like `episode_step`'s typed `action`. A candidate construction is a **proposed mathematical object, not a proof certificate**: its `trust_status` never certifies anything, and empirical support, human review, citation, and "a formal statement exists" all remain distinct from kernel verification. `add` proposes a construction (`graph_family`, `counterexample`, `coloring`, etc.) with motivated-discovery metadata — it can exist before a dossier, node, Lean theorem, or episode; `observe` records one empirical check (`supports`/`refutes`/`inconclusive`) against it, and never changes proof status; `update_status` updates status/trust_status/claimed_properties/known_failures/next_check (`kernel_verified_claim_linked` is rejected unless a real kernel-verified layer is already linked); `link_node` attaches it to a research node, adopting the node's dossier if the construction has none yet; `link_verification_layer` attaches it to an existing verification layer, adopting the layer's dossier if the construction has none yet — provenance, never promotion |
| `empirical_search` | ONE tool for the whole empirical math-lab family (issue #26), dispatching on an internally-tagged `action` (`add` / `observe` / `update_status` / `link_candidate` / `link_verification_layer`) — exactly like `episode_step`'s typed `action`. Every result is experimental **evidence, never proof**: no field carries kernel evidence, no status certifies an asymptotic/universal theorem, and even the strongest trust status only links to a formal target. `add` records a small-case/counterexample/construction search, parameter sweep, finite check, candidate ranking, or external-tool run; `observe` appends a finding and optional counterexample witness (`no_counterexample` never certifies a universal claim); `update_status` revises status/trust/results/candidate ids but cannot erase counterexamples, so falsified/failed/timed-out searches and witnesses stay visible; `link_candidate` and `link_verification_layer` attach existing dossier artifacts as provenance only — empirical support never proves a candidate, and a link never makes a layer kernel-verified |
| `challenge` | ONE tool for the challenge lifecycle (issue #53), dispatching on an internally-tagged `action` (`create` / `observe` / `update_status`) — exactly like `episode_step`'s typed `action`. A bounded, scored, reviewable competition frame for AI-generated math — never proof. `create` defines a challenge in an existing dossier, optionally linked to a problem_version/episode; `observe` reads it back with its tasks → submissions → scores/reviews, plus the export grouping (accepted/rejected/superseded/open separated), read-only; `update_status` sets open/closed/archived/superseded, never touching proof/fidelity/benchmark state. `validation_protocol_create` is dossier-scoped, not challenge-scoped, and remains its own tool below rather than folding into this one |
| `validation_protocol_create` | Register a validation protocol a task's submissions can be checked against. A protocol describes a check; it is never itself proof |
| `task` | ONE tool for the bounded-task lifecycle within a challenge (issue #53), dispatching on an internally-tagged `action` (`create` / `update_status`) — exactly like `episode_step`'s typed `action`. `create` adds a bounded task to a challenge (find_candidate_object, improve_bound, find_counterexample, classify_small_cases, produce_witness, minimize_example, maximize_parameter, verify_property, compress_strategy, distill_method, formalize_claim) — `bounds_json` keeps it small and reviewable; `update_status` updates a task's status (open/closed/superseded). A superseded task stays visible. Kept deliberately separate from `task_submission` (below) — a task is a bounded challenge assignment, a task_submission is a contribution submitted against a task |
| `task_submission` | ONE tool for the whole challenge-submission family, dispatching on an internally-tagged `action` (`create` / `validate` / `score` / `review` / `link` / `update_status`) — exactly like `episode_step`'s typed `action`. The variants carry **distinct trust profiles** and none is proof: `create` records an **untrusted** `content_json` payload (starts `submitted`); `validate` records an automated declared-check result (`validated`/`validation_failed` — **never** kernel verification; failed stays visible); `score` records a measurement (never proof; a rank is not proof authority; never confers training eligibility); `review` records a role-separated **human** decision (accepted/rejected/needs_changes/superseded — human review ≠ kernel verification, `accepted` means accepted into the dossier as a contribution, never proved); `link` records **provenance** to a candidate_construction / empirical_result / verification_layer in the submission's dossier (even a kernel_verified layer never makes the submission a proof); `update_status` sets the outcome (accepted/rejected/superseded/merged_into_dossier) without a review row. Rejected/superseded stay visible |
| `distilled_strategy_add` | Store a reusable distilled strategy artifact (cheat_sheet, heuristic_rule, counterexample_pattern, construction_recipe, …). A distilled strategy is **not** a proof; trust_status tops out at human_reviewed |
| `paper_ingest` | ONE tool for the whole paper/PDF ingestion family (issue #27), dispatching on an internally-tagged `action` (`create` / `extract_claims` / `observe` / `link_to_dossier` / `mark_review_status` / `link_node`) — exactly like `episode_step`'s typed `action`. Every action handles **untrusted extraction**, never proof: LLM-Driven Proof Search Environment does no OCR/LLM extraction — the host records its own extraction result, untrusted by construction, and **an extracted theorem is not statement-fidelity approval, an extracted citation is not citation validation, an extracted assumption is not an accepted assumption**. `create` ingests a paper/manuscript/proof-sketch/exposition as a reviewable source document, optionally linked to a dossier; `extract_claims` appends extracted nodes (main_theorem, definition, lemma, construction, reference, open_gap, …) — each node **requires** a non-empty `source_span` so it stays traceable to the source, plus confidence/status labels; `observe` reads a document with all extracted nodes and their trust labels (read-only); `link_to_dossier` attaches a document (and its nodes) to a dossier, so it surfaces in `research_dossier` `observe`'s ingestion bucket; `mark_review_status` updates a document's ingest/trust status, or (with `node_id`) a node's review/formalization/citation status (`rejected_extraction` stays visible; no status confers proof/fidelity/validation); `link_node` promotes/attaches an extracted node to a real dossier artifact — `external_reference` / `external_theorem_claim` (sets `citation_status=citation_recorded`), `research_node` / `formalization_plan_item` (sets `formalization_status=formalization_target_linked`) — recording provenance in the matching forward-link column and marking `review_status=linked_to_dossier_artifact`; the linked artifact keeps its own trust and the node **never** gains proof/kernel authority |
| `exposition` | ONE tool for the exposition-artifact family (issue #7), dispatching on an internally-tagged `action` (`add` / `observe`) — exactly like `episode_step`'s typed `action`. `add` records a human-readable exposition section (problem_summary, construction_intuition, key_lemmas, unverified_bridges, …) linked to a problem/episode/obligation/module/lemma/dossier — `prose_status` (prose/reviewed_prose/formalized) marks epistemic weight; prose is never proof and never changes certification or training eligibility; `observe` lists exposition artifacts for a problem_version, episode, or dossier — read-only prose, explicitly separate from kernel-verified proof |
| `semantic_skeleton` | ONE tool for the semantic-skeleton / module-aware-fidelity family (issue #6), dispatching on an internally-tagged `action` (`add` / `observe`) — exactly like `episode_step`'s typed `action`. `add` attaches a structured reading of a statement/module/solution (quantifiers, hypotheses, conclusion, definitions, construction map, back-translation, fidelity `risk_flags`) scoped by `review_scope`. Metadata only — never sets `fidelity_status` or substitutes for `problem_submit_fidelity_review`; `observe` appends one module-aware fidelity observation (confirms_faithful/raises_concern/reports_mismatch/inconclusive) to a skeleton's review history. `confirms_faithful` is not the root fidelity gate |
| `expert_review` | ONE tool for the expert-review ledger family (issue #14), dispatching on an internally-tagged `action` (`add` / `observe`) — exactly like `episode_step`'s typed `action`. Expert reviews are a **role-separated ledger of who reviewed what, not a substitute for kernel verification**. `add` records one review-ledger entry (proposer/construction_searcher/formalizer/prover/reviewer/domain_expert/refuter/editor/librarian) against a polymorphic target (source_problem, formal_statement, construction_artifact, module_artifact, external_citation, asymptotic_extraction, exposition, full_dossier) — a pure insert that never marks anything proved; `reviewer_id` is free text, not an authenticated principal; `observe` reads review-ledger entries back, filtered by dossier, target (kind+id), and/or reviewer role — revoked reviews are omitted unless `include_revoked=true`. Read-only |
| `mathlib_search_declarations` | Search the real pinned Mathlib source tree for declaration names containing a substring (beyond exact-name lookup). Advisory only |
| `mathlib_search_local_artifacts` | Search this instance's own previously-verified theorem/def names for a substring match |
| `run_envelope` | ONE tool for the whole run-envelope family (issues #34/#38/#46), dispatching on an internally-tagged `action` (`create` / `update` / `cost_observation_add` / `attach_episode` / `observe`) — exactly like `episode_step`'s typed `action`. Purely descriptive metadata; **no action ever affects proof status**. `create` records host/model/mode (development/evaluation/benchmark/private_audit/public_report) and host-side cost accounting LLM-Driven Proof Search Environment cannot itself observe, plus an origin cost observation; `update` corrects an envelope's host-side cost fields or notes after the fact — append-only (issue #46): a correction appends an auditable observation, so the prior value stays queryable; `cost_observation_add` appends an auditable, append-only host-side cost observation, never overwriting a prior one; `attach_episode` tags an episode with a run envelope (metadata only — never changes the episode's outcome/state) and enforces the mode-enforcement policy: an `attested`/`unsafe_dev_attestation` episode is unconditionally rejected from a benchmark/evaluation/public_report-mode envelope (no override), always allowed for `development`, and requires `allow_dev_attested=true` for `private_audit`; `observe` reads back an envelope, every episode tagged with it, and its full append-only cost-observation history |
| `benchmark_suite` | ONE tool for the benchmark-suite lifecycle (issues #29/#30/#65), dispatching on an internally-tagged `action` (`create` / `observe` / `set_trust`) — exactly like `episode_step`'s typed `action`. `create` registers a benchmark suite (e.g. PutnamBench) — name, upstream URL/commit, language, and a self-declared `trusted_canonical_source` flag (defaults false); `observe` reads back a suite by `suite_id`/`name` with its append-only trust-review history and (by default) every registered problem; `set_trust` changes `trusted_canonical_source` after creation — `approver_id` is required, raising trust to true **requires** non-empty `notes`, and every REAL change appends one audit row to `benchmark_suite_trust_reviews` (a same-value call is a recorded no-op). Never affects proof status of existing results — only the fidelity basis future `benchmark_result_record` calls can claim |
| `benchmark_problem` | ONE tool for the benchmark-problem lifecycle (issues #29/#30/#62/#65), dispatching on an internally-tagged `action` (`register` / `observe`) — exactly like `episode_step`'s typed `action`. `register` records one problem from a suite — `root_statement_hash` is server-computed from `root_formal_statement`, never client-supplied, and a `prover_ready_statement` (+ its own hash) is derived automatically (never client-supplied) when the statement is a `theorem NAME (binders) : type` declaration; `import_manifest` entries may be Lean module paths and/or `open [scoped] <Namespace> ...` directives (issue #62). `observe` reads back one registered problem by `benchmark_problem_id` or by (`suite_id`, `upstream_problem_id`), returning the full row including both hashes and the server-derived `prover_ready_statement` |
| `benchmark_run` | ONE tool for the whole benchmark-run family (issue #182's `benchmark_run_create`/`benchmark_result_record`/`benchmark_run_observe` consolidation), dispatching on an internally-tagged `action` (`create` / `result_record` / `observe`) — exactly like `episode_step`'s typed `action`. `create` starts a run against a suite; `lean_version`/`mathlib_commit` are read from the server's OWN detected Lean environment, never accepted from the client. `result_record` records (or upserts, for pass@k) one problem's result within a run — if `episode_id` is given, cross-checked against that episode's ACTUAL recorded outcome AND that it proved the SAME statement as the benchmark problem (issue #36), and a `kernel_verified`/`certified` claim additionally requires the issue #38 fidelity-basis policy (a trusted suite's own canonical statement-hash match, or an independently `fidelity_status='verified'` problem) — this trust boundary is unchanged by the consolidation. `observe` reads back a run, its results, and aggregate metrics — `solved_rate` (solved at all) vs `pass_at_1_rate` (genuine first-attempt success) are reported separately |
| `proof_session` | ONE tool for the whole interactive (tactic-by-tactic) proof-session family, dispatching on an internally-tagged `action` (`start` / `observe` / `tactic_step` / `branch` / `select_node` / `reconstruct` / `promote_to_attempt` / `close` / `export` / `replay`) — exactly like `episode_step`'s typed `action`. Search evidence only, except the `promote_to_attempt` action (and `replay` mode `final_proof`), which resubmits a reconstructed script through the real `attempt_claim` + `episode_step(Solve)` kernel-verification path. See [Interactive Proof Sessions](#interactive-proof-sessions) |
| `dev_diary` | ONE tool for the project-scoped dev diary family (issue #242), dispatching on an internally-tagged `action` (`create_project` / `attach` / `checkpoint` / `observe` / `export`) — exactly like `episode_step`'s typed `action`. Joins existing tracked evidence (problems, episodes, research dossiers, formalization plans, empirical searches, candidate constructions, verification layers, distilled strategies) into a chronological campaign timeline that a long-running effort can document as it happens. **This tool never calls an LLM and never posts anywhere** — it only assembles evidence for an external host to turn into a narrative. `create_project` starts a campaign (rejects a duplicate `project_key` rather than overwriting it); `attach` links an existing artifact by id (existence-checked against its own table) or an `external_link`/`public_post` URL, never altering the attached artifact's own trust/fidelity/outcome; `checkpoint` records a chronological, server-numbered milestone (success or failure) with an optional same-project attachment reference; `observe` reads back the project with every attachment/checkpoint plus a `resolved` view bucketing that same data into verified results, failed/blocked routes, reusable artifacts, surfaced claim boundaries, and the current frontier — purely re-bucketed from each artifact's own already-recorded status, never re-derived; `export` renders `structured_json` / `markdown_diary` / `x_thread_prompt` / `single_x_post_prompt` / `blog_prompt` / `institute_update_prompt`, gated by an explicit `x_tier`/`max_chars_per_post` (default `"free"` → 280 chars, X's real non-premium limit; `"premium"` → 25,000 — a caller override is always clamped DOWN to the tier's real ceiling, never up), supports a `since_checkpoint_id` cursor and `dry_run` preview, and records one immutable `dev_diary_publications` ledger row per non-dry-run call, hash-pinned for replay. See [Dev Diary](#dev-diary-project-campaigns) |

## Budget Accounting

Episode budgets are enforcement/accounting controls, not proof-soundness
claims. A `NULL` `episodes.cost_budget_micros` is unbounded; bounded budgets
are debited only by conditional reservations that must fit the current
remaining budget.

- `episode_step.cost_micros` is the environment step charge. It must be
  non-negative and is reserved before the step executes; over-budget steps are
  denied before any Lean gateway call.
- `model_call_reserve.reserved_cost_micros` is a host/model-call budget lease.
  It must be non-negative and immediately reserves bounded episode budget. The
  lease row is inserted only if that budget reservation succeeds.
- `model_call_settle(actual_cost_micros, status="settled")` records the
  caller-reported actual model-call cost. Settlement adjusts only the delta
  from the reservation: lower actual cost refunds the difference, higher actual
  cost conditionally debits only the extra amount.
- `model_call_settle(status="voided")` cancels a lease and refunds the full
  reserved amount; no actual model-call cost is reported for a voided lease.
- Reserved-but-unsettled costs remain reservations. Benchmark cost summaries
  continue to include only settled `actual_cost_micros` as attested
  `model_call_reported_cost_micros`, never as exact cost.

## Level 4 Research Substrate

Research dossiers are paper-scale working records for definitions, lemmas,
theorems, remarks, references, and open gaps. A dossier can be linked to a
`problem_version`, linked to an `episode`, linked to both, or created before
either exists.

The Level 4 substrate is explicit about trust boundaries:

- `proved_in_episode` means there is a linked Lean-verified episode lemma.
- `imported_from_mathlib` means the claim is attributed to Mathlib, not locally
  proved by this episode.
- `external_citation_unreviewed` and `external_citation_human_reviewed` are
  citation states, not proof states.
- `unformalized_assumption` and `rejected_unsafe_assumption` remain visible as
  assumptions or rejected assumptions.
- `verification_layers` track independent review/construction/formalization
  layers (arithmetic construction, geometric criterion, packing/size bound,
  asymptotic extraction, formal module, statement fidelity, external review, …)
  and can be `blocked` or `failed` without failing the whole dossier. A layer
  reaches `kernel_verified` only for a `formal_module`/`statement_fidelity`
  layer backed by a real Lean pass — a search/construction/packing layer never
  can. The markdown-family `proof_export` modes render a **Verification layers**
  table for the dossier(s) attached to the episode or its problem, and
  `training_export` carries the same per-layer state as structured,
  redacted metadata (`layer_kind`/`status`/`target_kind`/redacted
  `target_handle`/`summary` plus `kernel_verified_layer_count`/
  `total_layer_count` and the non-gating policy note) alongside its `records`
  array — so every export reports the true per-layer state, not only the
  episode outcome. Layer status is **additive metadata**: a kernel-verified
  root theorem does not imply every layer is verified, and layer completeness
  never gates `certified`.

No cited, reviewed, empirical, or assumed artifact is represented as kernel
verified unless it is linked to an actual Lean-verified artifact. These tables
are research bookkeeping and do not mutate episode outcome, obligation status,
budget state, fidelity status, or benchmark results.

### Candidate construction artifacts

Candidate constructions are proposed mathematical objects — graph families,
point configurations, colorings, field towers, lattices, counterexamples,
asymptotic families, algebraic objects, combinatorial designs, and so on. They
are the first durable object layer for **motivated discovery**: beyond *what*
object is proposed, each records *why* it was proposed and what to do with it,
encoding the loop

```text
observation → motivated move → proposed object → intended role → next check
```

via the fields `motivating_move` (`generalize`, `specialize`, `decompose`,
`search_extremal_example`, `search_counterexample`, `introduce_invariant`,
`reduce_to_known_theorem`, …), `source_observation`, `intended_role`
(`witness`, `counterexample`, `extremal_example`, `lower_bound_construction`,
`formalization_target`, `bridge_to_existing_theorem`, …), `strategy_context`,
`why_this_might_work`, `why_this_might_fail`, `next_check`, and
`future_challenge_relevance`. The object itself lives in `informal_description`,
`parameters_json`, and `construction_json`; `verification_targets_json` records
what a later system should check.

A candidate construction can exist before there is a research dossier written
up, before there is a Lean theorem, before there is an episode, and before
there is empirical search machinery to generate one automatically (that
machinery is issue #26's empirical math lab; this substrate only holds the
objects it will produce and judge). Every link — `dossier_id`,
`related_node_id`, `verification_layer_id`, `problem_version_id`,
`episode_id` — is optional.

Candidate constructions are **not proof certificates**. Their `trust_status`
makes that explicit:

- `informal`, `empirical_evidence`, `cited`, `human_reviewed`, and
  `formalized_statement_exists` are all states short of kernel verification —
  empirical support, human review, a citation, or even an existing formal
  statement are each distinct from, and never imply, being proved.
- `kernel_verified_claim_linked` is the only state that claims kernel
  evidence, and it is rejected unless the construction's
  `verification_layer_id` names a `verification_layers` row whose own status
  is already `kernel_verified` (itself only reachable through real
  Lean-backed evidence — see above). A candidate construction can link to
  real evidence; it can never manufacture it.

A candidate construction can attach to a dossier, a research node, and/or a
verification layer, or exist attached to none of them. `falsified` and
`rejected` constructions stay visible in `research_dossier`'s `observe` action
rather than being deleted, since a documented dead end is itself research
output.

### Exposition artifacts

Serious mathematical output is not only a Lean file — it needs an explanation
layer: what the construction means, why the definitions were chosen, what the
key lemma does, and what remains unformalized. Exposition artifacts capture
that prose **alongside, and explicitly separate from, kernel-verified proof**.
Each carries a `prose_status` making its epistemic weight explicit:

- `prose` — raw author narrative.
- `reviewed_prose` — a human read it.
- `formalized` — the described claim is backed by a linked formal artifact.

**None of these is kernel verification**, and no exposition artifact ever
changes an episode outcome, `fidelity_status`, canonical promotion, training
eligibility, budget, or benchmark state. `proof_export` renders exposition in
its own `## Exposition (prose — not part of the verified proof)` section,
never inside the proof tree or the verified-module source, and every section
is labeled with its `prose_status` so a reader can never mistake reviewed or
unreviewed narrative for a checked proof. An artifact can attach to a
problem, an episode, a specific obligation, a verified module, a verified
helper lemma, and/or a research dossier — every link is optional.

### Semantic skeletons (module-aware fidelity)

Statement fidelity can't stay a single flat approval over one root
proposition: a module can prove a correct formal theorem while the real source
claim still rests on prose-only bridges (integer encoding, a bijection, a
final-answer extraction, a domain restriction). A **semantic skeleton** is a
structured reading of what a statement, verified module, or source-aligned
solution actually says — `quantifiers`, `hypotheses`, `conclusion`,
`definitions`, `construction_map`, a natural-language `backtranslation`, and
fidelity `risk_flags` — scoped by `review_scope` (`root_statement_only`,
`module_artifact`, `source_aligned_solution`, `computational_check_only`,
`structural_proof`). Its `semantic_fingerprint_hash` is server-computed over
the normalized content, never client-supplied.

A skeleton is **descriptive metadata, never the fidelity gate**: it has no
column that can hold kernel evidence, never sets `fidelity_status`, and never
substitutes for `problem_submit_fidelity_review`. `semantic_skeleton`'s
`observe` action appends module-aware review notes (`confirms_faithful`,
`raises_concern`, `reports_mismatch`, `inconclusive`) — a `confirms_faithful`
note is note-taking, not a proof.

### Expert reviews (role-separated ledger)

Serious mathematics gets its credibility from more than one prover: a claim is
proposed, formalized, proved, refereed, and checked by domain experts.
**Expert reviews** are a role-separated ledger of who reviewed what and what
they decided — `reviewer_role` (proposer, construction_searcher, formalizer,
prover, reviewer, domain_expert, refuter, editor, librarian) against a
polymorphic `review_target_kind` (source_problem, formal_statement,
construction_artifact, module_artifact, external_citation,
asymptotic_extraction, exposition, full_dossier), with a `decision`,
`confidence`, `expertise_tags`, `requested_changes`, and `risk_flags`.

`expert_review`'s `add` action is a **pure insert**: unlike `research_dossier`'s
`citation_review_add` action (which updates a citation's `claim_status`), an
expert review mutates no other table.
`reviewer_id` is free text, not an authenticated principal, and a
`domain_expert` "approved" decision is human-attested — it never marks
anything kernel-verified, never changes an episode outcome, `fidelity_status`,
canonical promotion, budget, or benchmark state. A `rejected` review records
an opinion without deleting or downgrading the reviewed artifact.

### Empirical math lab (issue #26)

The empirical math lab records **experimental mathematical evidence** —
small-case searches, counterexample searches, construction searches, finite
model checks, parameter sweeps, and candidate rankings. It is the object layer
candidate constructions are generated, tested, ranked, and falsified against.
It helps discover patterns, candidates, counterexamples, and next proof
targets. **It does not prove theorems. It does not certify asymptotic claims.
It does not replace Lean/kernel verification.**

That boundary is structural, not a convention:

```text
empirical evidence          ≠ proof
small-case check            ≠ asymptotic theorem
no counterexample found     ≠ universal theorem certified
successful construction     ≠ its claimed properties proved
candidate ranking           ≠ verified claim
human-readable result       ≠ kernel verification
```

An `empirical_searches` row has no column that can hold kernel evidence;
`has_kernel_evidence` and `is_proof` are always false. `trust_status` tops out
at `linked_to_formal_target` ("this evidence points at a formalization
target") — still not a proof. Every link (`dossier`, `research_node`,
`candidate_construction`, `verification_layer`, `problem_version`, `episode`)
is optional, so a search can exist before any dossier, candidate, episode, or
Lean proof. `counterexamples`, `failed`, and `timed_out` searches stay visible
(a documented dead end is research output). `cost_summary`/`runtime_metadata`
describe the *external* search run and are isolated from LLM-Driven Proof Search Environment's own cost
surfaces. `research_dossier`'s `observe` action surfaces empirical searches in
their own bucket, separate from proofs, citations, assumptions, candidate
constructions, expert reviews, semantic skeletons, exposition, and verification
layers.

### Paper/PDF ingestion (issue #27)

The empirical math lab and research substrate become useful *before* a Lean
formalization exists when LLM-Driven Proof Search Environment can turn a paper, manuscript, model-written
proof sketch, or human exposition into a structured research workspace. Paper
ingestion records an `ingested_documents` source plus its extracted
`ingested_document_nodes` (abstract, main_theorem, definition, proposition,
lemma, proof_step, construction, remark, appendix_fact, reference, open_gap),
each with a **required** non-empty `source_span` back to the paper text (so no
node is untraceable), a `confidence`, and `formalization_status` /
`citation_status` / `review_status` labels.

**LLM-Driven Proof Search Environment does no OCR/LLM extraction itself** — no inference code lives here. The
host performs extraction and records the structured result, which is **untrusted
by construction**. Ingestion is not verification, and the boundary is
structural:

```text
PDF ingestion            ≠ proof
OCR/LLM extraction        = untrusted
extracted theorem text   ≠ statement-fidelity approval
extracted citation       ≠ citation validation
extracted assumption     ≠ accepted assumption
```

Neither table has a column that can hold kernel evidence; `is_proof` /
`has_kernel_evidence` / `is_statement_fidelity_approved` are always false, and
`formalization_status` is CHECK-constrained to `prose_only` /
`formalization_pending` / `formalization_target_linked` — it can never reach a
proved/verified value. `extraction_trust_status` (unreviewed → machine_extracted
→ human_reviewed_extraction / rejected_extraction / linked_to_dossier_artifact)
tops out at human review, never Lean verification. A `rejected_extraction` stays
visible (never deleted). Extracted nodes are *candidates* that must go through
the normal Lean / fidelity-review / citation / external-theorem paths to gain
any authority. `paper_ingest`'s `link_node` action records that promotion explicitly:
it attaches a node to an `external_reference`, `external_theorem_claim`,
`research_node`, or `formalization_plan_item` that **already exists** (and, for
dossier-scoped kinds, belongs to the document's dossier), setting the node's
derived `citation_status` / `formalization_status` and stamping the matching
forward-link column — but the linked artifact keeps its own independent trust
and the node still gains no proof/kernel authority.
`research_dossier`'s `observe` action shows ingested documents and their nodes
in their own bucket, separate from every proof-bearing bucket.

**Benchmark contamination policy:** upstream benchmarks like PutnamBench ask
that completed formal proofs not be published without first coordinating with
their maintainers. See [docs/benchmarks/putnambench.md](docs/benchmarks/putnambench.md)
for how `proof_export`'s modes and `allow_putnambench_proof_export` flag
enforce this.

### Challenge / task / scoring substrate (issue #53)

AI can generate far more mathematical material than humans can review as full
proofs. Instead of giant opaque proof dumps, LLM-Driven Proof Search Environment channels contributions into
small, bounded, typed, scored, reviewable units:

```text
research_dossier → challenge → task → submission → validation → score → review → distilled artifact
```

A dossier defines a `research_challenge`; a challenge defines bounded
`research_tasks` (`find_candidate_object`, `improve_bound`, `find_counterexample`,
`classify_small_cases`, `produce_witness`, `minimize_example`,
`maximize_parameter`, `verify_property`, `compress_strategy`, `distill_method`,
`formalize_claim`), each with a `bounds_json` that keeps it small; a task accepts
`research_task_submissions` (untrusted `content_json`); a submission is
`validated` against a `validation_protocol`, `scored` (`scoring_results`), and
`reviewed` (`review_results`); accepted work links back to a
`candidate_construction` / `empirical_result` / `verification_layer` as
provenance; and reusable method knowledge is compressed into
`distilled_strategy_artifacts` (`strategy_cheat_sheet`, `heuristic_rule`,
`counterexample_pattern`, `construction_recipe`, `formalization_hint`, …).

**Trust boundary (structural).** Every table here is research bookkeeping — no
column can hold kernel evidence:

```text
challenge/task/score       ≠ proof
accepted submission        ≠ proof
scored submission          ≠ proof
validated empirical result ≠ kernel verification
leaderboard rank           ≠ proof authority
distilled strategy         ≠ proof
```

`is_proof` / `has_kernel_evidence` are always false on every challenge, task,
submission, score, and review; a challenge **score alone never confers training
eligibility**; submission status can never reach a proof value; a link to a
kernel-verified `verification_layer` records provenance only and never makes the
submission a proof. A rejected or superseded submission stays visible (never
deleted), and `challenge`'s `observe` action exports the work grouped by outcome
(accepted / rejected / superseded / open shown separately). Only Lean / kernel
verification creates proof authority; challenge state never gates `certified`.

## `Solve` vs. `SubmitModule`

As of v0.3.x, `episode_step` accepts more than a single theorem body:

- **`Solve { proof_term, proof_format? }`** — one theorem: `theorem O_<id> : <statement> := by <proof_term>`. Good for a self-contained tactic proof. `proof_format` (issue #51) is an optional whitespace-transport hint: `flat_tactic_sequence` (default) flattens accidental nesting; `raw_lean_block` preserves the proof's relative indentation for intentional focus-bullet/nested-block structure. It only affects leading whitespace — the Lean kernel remains the sole authority. `SubmitModule`'s `root_theorem` accepts the same field.
- **`SubmitModule { module_items, root_theorem }`** — a small local Lean *development*: helper `def`s, helper `theorem`s, and a root theorem, assembled by the server into one namespaced module and verified as a unit. `module_items` is a list of:
  - `LeanModuleItem::Def { name, type_signature, body }` — `def <name> : <type_signature> := <body>`
  - `LeanModuleItem::Theorem { name, statement, proof_term }` — `theorem <name> : <statement> := by <proof_term>`
  - `LeanModuleItem::MutualGroup { members }` — 2+ `Def`/`Theorem` members that must forward-reference each other (e.g. mutually recursive functions), rendered together inside one server-owned `mutual ... end` block.

The trust boundary is the same one the single-theorem path already has, one
level up: **the model proposes, the server assembles, Lean verifies, the
ledger records.** A client never writes raw Lean — no `import`/`namespace`/
`end`/`set_option` lines, no `axiom`/`opaque`/`unsafe`/`instance`
declarations, never `mutual`/`end` directly (the server owns those tokens
even for a `MutualGroup`). Every name is sanitized to a single namespace-local
identifier, and `root_theorem.statement` must canonical-hash to the problem's
registered root formal statement — a module can never silently prove a
different goal. Verification is **staged and all-or-nothing**: either the
whole module passes the kernel and is recorded, or nothing enters the trusted
namespace.

```jsonc
{
  "type": "submit_module",
  "module_items": [
    { "item_kind": "def", "name": "double", "type_signature": "Nat → Nat", "body": "fun n => n + n" }
  ],
  "root_theorem": { "name": "root", "statement": "double 2 = 4", "proof_term": "rfl" }
}
```

Proof soundness vs. statement fidelity (below) is unchanged for module
proofs — a `SubmitModule` root proof reaches the same `kernel_verified`/
`certified` outcomes a `Solve` proof does. A verified module is also a
first-class replayable artifact: `proof_export(format="lean")` can emit the
exact verified module source, and `episode_replay` re-assembles it from the
recorded structured items and re-verifies against the kernel. Full detail,
including the mutual-recursion trust boundary and injection hardening: see
[`docs/submit_module.md`](docs/submit_module.md). For what level of capability
this represents and what's still missing, see [`docs/roadmap.md`](docs/roadmap.md).

## Dev Diary (Project Campaigns)

A long-running campaign (issue #242) — a single Erdős problem worked over
weeks, say — spans hundreds of problems, episodes, dossiers, and diagnostic
dead ends. Reconstructing that story after the fact from a chat transcript is
slow and error-prone. `dev_diary` is a project-scoped layer that joins
existing tracked evidence into a chronological timeline as the campaign
happens, and can export a grounded packet plus a ready-to-use prompt for an
external host to turn into an X thread, a blog post, or an institute update.

**`dev_diary` itself never calls an LLM and never posts to X or anywhere
else.** It has no provider SDKs, no API keys, no network client — the same
boundary this whole environment holds everywhere else. It assembles evidence;
an external agent host (Claude Code, or whatever is calling this tool) writes
the prose and decides whether/where to publish it.

- `create_project` starts a campaign keyed by a unique, human-stable
  `project_key` (e.g. `erdos-647`). A duplicate key is rejected, never
  silently overwritten.
- `attach` links an existing first-class artifact — a `problem_version`,
  `episode`, `research_dossier`, `formalization_plan`, `empirical_search`,
  `candidate_construction`, `verification_layer`, or `distilled_strategy` — by
  id, existence-checked against that artifact's own table. `external_link` and
  `public_post` (a GitHub issue/PR URL, or a manually recorded public post)
  carry an `external_url` instead, since neither has a backing row. Attaching
  is provenance only: it never reads back, alters, or upgrades the attached
  artifact's own `trust_status`/`fidelity_status`/outcome.
- `checkpoint` records one chronological milestone — `campaign_started`,
  `candidate_found`, `proof_attempt_failed`, `root_cause_identified`,
  `kernel_result`, `mathlib_gap`, `method_exhausted`, `frontier_changed`,
  `claim_corrected`, `infrastructure_issue_opened`, `public_update_posted`, or
  `other` — with a human/agent note and an optional same-project attachment
  reference. `checkpoint_number` is assigned server-side (never
  caller-supplied), so chronological order is guaranteed regardless of client
  behavior. Failed and negative checkpoints are preserved exactly like
  successful ones, the same append-only posture as `reasoning_log`.
- `observe` reads the project back with every attachment and checkpoint in
  order, plus a `resolved` view: `verified_results` (attachments whose
  underlying `episode.outcome` is already `certified`/`kernel_verified`, or
  whose `verification_layer.status` is already `kernel_verified`),
  `failed_or_blocked` (matching failure outcomes/statuses, plus
  `proof_attempt_failed`/`method_exhausted` checkpoints), `reusable_artifacts`
  (attached `formalization_plan`/`distilled_strategy` rows),
  `claim_boundaries` (each attached dossier's own `assumption_boundaries`,
  unchanged), `checkpoints_by_kind`, and `current_frontier` (the latest
  `frontier_changed` note). Every bucket is re-derived purely from columns
  already recorded elsewhere — `observe` never re-decides a trust status.
- `export` renders the project as `structured_json` (full detail, internal
  ids retained, for grounding/audit), `markdown_diary` (a human-readable
  document), or one of four external-host prompts — `x_thread_prompt`,
  `single_x_post_prompt`, `blog_prompt`, `institute_update_prompt` — each
  populated with the resolved packet and an instruction not to surface raw
  database ids in the generated prose. The two X modes are gated by an
  explicit `x_tier` (`"free"` or `"premium"`, defaulting to `"free"` whenever
  omitted — the conservative assumption, since most callers will not have a
  paid account) resolving to `max_chars_per_post` (280 for free, X's real
  non-premium limit; 25,000 for premium): a caller-supplied override is always
  clamped DOWN to the resolved tier's ceiling, never allowed past it. A
  `since_checkpoint_id` cursor scopes an export to checkpoints after a given
  checkpoint (attachments are not cursored — they are not chronological in
  that sense). Unless `dry_run`, every export records one immutable
  `dev_diary_publications` row (mode, cursor, resolved `x_tier`/
  `max_chars_per_post`, and a canonical hash of the exact packet) so a later
  audit shows precisely what a given thread was generated against.

## Interactive Proof Sessions

Alongside the whole-proof-attempt actions above (`Solve`, `SubmitModule`,
`Decompose` — all submitted through `episode_step`), the single
`proof_session` tool (issue #161's family, consolidated into one
internally-tagged-action tool by issue #183; part of the
interactive-proof-session epic #158) lets a client work **one** obligation's
goal state tactic-by-tactic — Pantograph-style live proof-state interaction —
instead of only submitting a complete proof and finding out afterward whether
it checked. Every call has the shape
`proof_session {"action": {"type": "<variant>", ...}}`, exactly like
`episode_step`'s typed `action`.

### How this differs from `Solve` / `SubmitModule` / `Decompose`

- **`Solve`** and **`SubmitModule`** are whole-proof-attempt submissions: you
  hand the server a complete tactic script (or module) and the real Lean
  kernel checks it in one pass, via `episode_step`. This remains the only
  family of actions that can mark an obligation `kernel_verified`/`certified`.
- **`Decompose`** splits the current obligation into child sub-lemma
  obligations — still a real, budget-accounted `episode_step` action with no
  session state involved.
- **`proof_session`** sits *beside* `episode_step`, not on top of it: its
  actions let you explore a goal state one tactic at a time, branch to try
  alternatives from an earlier point, and see whether a path closes
  (`is_solved: true`) before committing to a `Solve`/`SubmitModule`
  submission. Nothing in this family changes how `Solve` / `SubmitModule` /
  `Decompose` / `GiveUp` behave, and — with one deliberate exception below —
  no `proof_session` action can change an obligation's status.

### What each action does

| Action (`{"action": {"type": ...}}`) | What it does | Category |
|---|---|---|
| `start` | Starts a new session against one existing episode obligation, backed by an `InteractiveProofGateway` backend (`mock` or `pantograph`). Returns a `session_id` and the root proof-state node. | Starts a session, records initial evidence |
| `observe` | Reads back the session's currently selected node — goals, local context, proof-state hashes, branch summary. | Read-only, records nothing new |
| `tactic_step` | Applies one tactic to a node. Success records a new child node as evidence and moves the session's selected node forward; failure records a structured diagnostic — also evidence, never discarded, a first-class negative example. | Records evidence, advances working state |
| `branch` | Same mechanics as `tactic_step`, framed explicitly as starting a *named* branch from any existing node. Prior branches from the same parent are never deleted or overwritten. | Records evidence, advances working state |
| `select_node` | Moves the session's "selected node" convenience pointer to any existing node in its tree (e.g. to switch which branch you're working). Applies no tactic and records no new evidence. | Working state only |
| `reconstruct` | Builds a Lean tactic script from the root-to-selected-node path and returns it verbatim (raw tactic text for a successful step is *not* durably stored server-side otherwise). `reports_complete` reflects the session's *own* `is_solved` claim — still not a verified proof. | Reconstructs a proof, still search evidence |
| `promote_to_attempt` | **The only action in this family that can change an obligation's status.** Takes a reconstructed script and resubmits it through the exact same `attempt_claim` + `episode_step(Solve)` path a normal whole-proof submission uses — a real, from-scratch Lean kernel check. | Final verification |
| `close` | Marks a session `closed` / `abandoned` / `superseded`. The session's full trace (every node/step, including failed tactics) stays visible and queryable afterward — closing never deletes anything. | Session lifecycle only |
| `replay` | Replays a session from *persisted DB state* in one of three modes: `trace_only` (pure DB-consistency check, no kernel call), `backend` (re-runs the tactic path against a fresh backend session and compares outcomes/hashes), `final_proof` (resubmits through the real verification path). | `trace_only`/`backend`: evidence check only. `final_proof`: final verification |
| `export` | Exports one session's trace as `public_summary` (aggregate counts only, no tactic/goal text), `audit_archive` (full trace, hashes, reconstructed-script linkage), or `training_export` (per-step records including negative-space failed routes). | Read-only export of already-recorded evidence |

### The loop

```text
proof_session {"action": {"type": "start", ...}}
    │  (root node)
    ▼
proof_session {"action": {"type": "tactic_step" / "branch" / "select_node", ...}}   ← repeat, explore, branch
    │  (some node reports is_solved: true)
    ▼
proof_session {"action": {"type": "reconstruct", ...}}          ← builds a tactic script from root → selected node
    │
    ▼
proof_session {"action": {"type": "promote_to_attempt", ...}}   ← the ONLY step that can change obligation status:
                                                                     attempt_claim + episode_step(Solve) through the
                                                                     real Lean kernel, exactly like a direct Solve call
```

The `replay` action with `mode="final_proof"` is an alternate route to the
same trust gate for a closed or historical session — it reconstructs and
resubmits through the same internal `attempt_claim` + `episode_step(Solve)`
logic, not a second, parallel verification path.

### The trust boundary

**Every `proof_session` result — a session's state, a tactic-application
outcome, a reconstructed script, a replay result — is search evidence, never
proof authority.** A node reporting `is_solved: true` is only the session's
own internal claim; the deterministic `mock` backend (the only backend that
actually steps tactics today) closes the first open goal on every
syntactically nonempty tactic string, without ever asking a real elaborator
whether that tactic discharges the goal. The only way an interactive session
can change an obligation's status is the `reconstruct` action followed by
`promote_to_attempt` (or `replay` with `mode="final_proof"`) — both route
through the exact same `attempt_claim` + `episode_step(Solve)` internal path,
the real Lean kernel, that every direct `Solve` submission already uses. If a
future backend's own elaborator ever disagrees with the kernel, the kernel
wins, always.

Do not report a goal as proved, or an obligation as closer to done, based on
`tactic_step` / `observe` / `branch` / `select_node` / `reconstruct` output
alone — only a `promote_to_attempt` (or `replay` `mode="final_proof"`) result
backed by a real kernel verdict counts.

### Backend choices

- **`mock`** (default) — a deterministic, in-memory test double: no Lean
  process, no Pantograph, no I/O. Always available; useful for exercising the
  full start → step → branch → reconstruct → promote loop mechanically, but
  its tactic outcomes carry no real elaboration evidence — it closes the
  first open goal on any nonempty tactic string, correct or not.
- **`pantograph`** — a *recognized* backend value, not yet a *usable* one.
  `PantographInteractiveGateway` (issue #166) runs a real filesystem/PATH
  probe for a compatible Pantograph installation (binary on `PATH`,
  `lake-manifest.json` dependency, a fetched checkout, a matching
  `lean-toolchain`) and reports specifically which of those conditions is
  missing — but this prototype has no process-spawning/IPC implementation
  behind it, so every operation fails closed regardless of what the probe
  finds, including the most favorable case (a fetched Pantograph checkout
  whose toolchain matches this project's own exactly). Check
  `environment_describe`'s `pantograph_available` / `pantograph_reason`
  fields before assuming Pantograph is usable in a given environment —
  `pantograph_available` is `false` in every configuration this prototype can
  currently detect.

Results from either backend remain subject to the trust boundary above
regardless of how "confident" the backend's own internal state looks.

See [`docs/roadmap.md`](docs/roadmap.md)'s Level 2.5 section for where this
capability sits relative to whole-module verification (Level 2) and
formalization planning (Level 3), and how its failed-tactic records feed
negative-space training/export value.

## Drafts and formalization planning (Level 3)

Before a `Solve`/`SubmitModule` attempt, a client can preserve informal
reasoning as a **Draft** (`draft {"action": {"type": "create", ...}}`) and
record the moves it identifies within it (`draft {"action": {"type":
"extract_moves", ...}}` — construction, auxiliary_lemma, case_split,
induction, reduction, bijection, counterexample_search, asymptotic_step,
external_citation, unknown). Since issue #195 the whole draft family is the
single `draft` tool, dispatching on an internally-tagged action
(`create` / `observe` / `extract_moves`), exactly like `episode_step`.
Selected moves can seed a **formalization plan** — since issue #184 the whole
plan family is the single `formalization_plan` tool, dispatching on an
internally-tagged action (`formalization_plan {"action": {"type": "create",
...}}`, exactly like `episode_step`) — which tracks planned concepts,
definitions, lemmas, and modules together with their Mathlib coverage status
(the `attach_lookup`
action, using `lean_declaration_lookup` results, or the
`attach_librarian_result` action, using `mathlib_search_declarations` /
`mathlib_search_local_artifacts` results).

Both are strictly advisory, mirroring the trust boundary everywhere else in
this environment: a Draft or a plan item can never mark anything proved.
Real obligations are still created only through `Decompose`, via the normal
budget-accounted `episode_step` flow — the `promote_item_to_obligation`
action only records a metadata *link* to an obligation that already exists
that way; it never creates one itself. See `docs/roadmap.md`'s Level 3
section for the full design.

## Proof soundness vs. statement fidelity

These are independent claims, and the environment never conflates them:

- **Proof soundness** — the Lean kernel verified this exact formal statement. Reaching this alone yields `outcome: "kernel_verified"`.
- **Statement fidelity** — that formal statement actually represents the source problem. Only `problem_submit_fidelity_review(decision="verified")` can establish this, based on evidence the server independently hash-checks against the problem's *current* source/statement/rendering (a stale or mismatched submission is rejected, not silently accepted).

`outcome: "certified"` requires **both** — a kernel-verified root can never present as certifying the source claim on proof soundness alone. This closes a real exploit: a trivially-true weakening of a source problem (e.g. proving `∀ n, Even n → True` for the claim "every even natural is divisible by two") kernel-verifies but must never be reported, rewarded, or exported as if it certified the source claim. See `docs/fix_plan_playtest_02.md`.

Two ways to unlock proving:
- **Real review**: `problem_submit_fidelity_review(decision="verified", ...)` → `fidelity_status="verified"` → root proof reaches `certified` directly (or promotes retroactively if the root was already `kernel_verified`).
- **Dev bypass**: `problem_create(unsafe_dev_attestation=true)` → `fidelity_status="attested"` → proving is allowed, but the episode can only ever reach `kernel_verified`, never `certified` — and problems/episodes under `attested` are excluded from default dataset exports (`training_eligible=false`).

A minimal prover loop is: `problem_create` → `problem_submit_fidelity_review` (or `unsafe_dev_attestation=true` for dev use) → `episode_create` → `episode_observe` → `attempt_claim` → `episode_step` → repeat `episode_observe`/`attempt_claim`/`episode_step` until `outcome` is set.

## Import manifests and "environmental scope collapse"

Every problem version has an immutable import manifest — the exact set of Mathlib modules its proofs are checked against (base: `Mathlib.Tactic.Ring` + `Mathlib.Tactic.NormNum`; extend it via `problem_create(problem_imports=[...])`, each validated with a real compile check before acceptance). Import strings and `lean_declaration_lookup` names are written verbatim into Lean source, so both are restricted to plain identifier syntax (dot-separated `[A-Za-z_][A-Za-z0-9_]*` segments for imports; no whitespace/comment/command syntax for declaration names) and capped at 50 entries per call — anything else is rejected before it ever reaches Lean, never silently compiled. See `docs/fix_plan_playtest_04.md`.

**An `unknown_declaration` diagnostic only ever proves a name didn't resolve under that exact manifest — it never proves the name is absent from the pinned Mathlib.** Before either changing proof strategy or declaring an API unavailable, call `lean_declaration_lookup`.

By default the lookup only checks the problem's own manifest — a few seconds, since it doesn't load all of Mathlib:

- **`available`** — resolves under the current manifest.
- **`not_available_under_current_manifest`** — doesn't resolve under the current manifest. **This alone does not prove absence from the library** — call again with `deep_check=true` to get a conclusive verdict.
- **`environment_error`** — the lookup itself failed; not evidence either way.

Pass `deep_check=true` to additionally check under the full Mathlib umbrella (slow — reliably 15-40+ seconds, since it loads all of Mathlib) and get a conclusive verdict:

- **`not_in_current_import_scope`** — resolves under the full umbrella but not the current manifest → add the module via a new `problem_create(problem_imports=[...])`.
- **`unknown_declaration`** — doesn't resolve even with everything imported → genuinely try a different name.

Conflating "not available under the current manifest" with "the library doesn't have this" — is a real failure mode we call **environmental scope collapse**: a local fact about one import closure gets inflated into a global claim about library capability, which can cascade into a model abandoning a provable branch. `environment_describe` carries this as an explicit epistemic rule for any agent driving the loop. Diagnostics also distinguish `unknown_declaration` (name resolution) from `parse_error` (syntax) and other categories — see `docs/fix_plan_playtest_03.md`. The fast-default/opt-in-deep split exists because the unconditional umbrella check was slow enough to blow past MCP client tool-call timeouts — see `docs/fix_plan_playtest_04.md`.

Import manifests are immutable per problem_version and included in every observation/trajectory event as `import_manifest_hash`, so replay always re-verifies against the exact closure the original attempt used.

## Prerequisites

- **Rust** (2024 edition) — install via [rustup](https://rustup.rs/)
- **Lean 4 toolchain manager (elan)** — install via [elan](https://github.com/leanprover/elan):
  ```powershell
  # On Windows, you can use the included bootstrap script:
  .\elan-init.ps1
  ```
- **The `lean-checker` Lake project** — see [Lean Checker Setup](#lean-checker-setup) below. Without it, `solve` actions fail with an infrastructure error; every other tool (episode lifecycle, decompose, trajectories, dataset export) works without it.

## Lean Checker Setup

`PROOFSEARCH_LEAN_PROJECT_PATH` (default `./lean-checker`) must point at a [Lake](https://github.com/leanprover/lake) project that depends on [Mathlib](https://github.com/leanprover-community/mathlib4). Every problem version has its own immutable **import manifest** — the exact Mathlib modules its proofs (and its `SubmitModule` developments) are checked against, starting from a base of `Mathlib.Tactic.Ring` + `Mathlib.Tactic.NormNum` (`omega` comes with core Lean once any Mathlib module is imported) and extendable per-problem via `problem_create(problem_imports=[...])` — each additional module is validated with a real compile check before the problem is accepted, not merely a name-shape check (`crates/proofsearch-core/src/lean/mod.rs`). This is not a single hardcoded import list baked into the gateway; see [Import manifests and "environmental scope collapse"](#import-manifests-and-environmental-scope-collapse) above. Setting up the Lake project itself is a one-time, multi-gigabyte task — do it once per machine, not per session:

```powershell
# 0. (Optional but recommended on machines with a small C: drive) Keep the multi-GB
#    toolchain store off the system drive. Match this with PROOFSEARCH_ELAN_HOME in the
#    MCP server env so the server's Lean subprocesses resolve the same store.
$env:ELAN_HOME = "F:\lean\elan"

# 1. Scaffold a Lake project pinned to Mathlib's toolchain (skip if lean-checker/ exists).
#    The math template runs `lake update` itself, cloning mathlib + deps.
lake +leanprover-community/mathlib4:lean-toolchain new lean-checker math
cd lean-checker

# 2. Download Mathlib's prebuilt .olean cache (do NOT build from source —
#    that takes hours; the cache download takes minutes)
lake exe cache get

# 3. Verify the toolchain resolves and a trivial proof compiles
@'
import Mathlib.Tactic.NormNum
theorem t : (1:Nat) + 1 = 2 := by norm_num
'@ | Out-File -Encoding utf8 smoke.lean
lake env lean --json smoke.lean
```

If step 3 prints no `"severity":"error"` JSON lines, the gateway is ready. Point `PROOFSEARCH_ELAN_BIN_PATH` at the `.elan/bin` directory containing `lake.exe`/`lean.exe` (default `~/.elan/bin`), and `PROOFSEARCH_LEAN_PROJECT_PATH` at the `lean-checker/` directory itself (the one containing `lakefile.toml`). The server checks both paths at startup and reports readiness via `environment_describe`'s `lean_gateway` field (`"ready"` or `"unavailable"`) — an `"unavailable"` warning is also printed to stderr on stdio startup.

The gateway copies every kernel-passing proof into `lean-checker/LeanChecker/Verified/O_<id>.lean` and `lake build`s it so later obligations can `import` it as an approved dependency — keep that directory out of `.gitignore` exclusions if you want to inspect proved lemmas after a run.

## Build

```bash
# Debug build (fast compile, slower runtime)
cargo build

# Release build (optimized binary)
cargo build --release
```

The MCP server binary will be at:
- Debug: `target/debug/proofsearch-mcp.exe`
- Release: `target/release/proofsearch-mcp.exe`

## Run Tests

```bash
cargo test
```

This runs the full test suite across both crates:

| Test Suite | What It Verifies |
|---|---|
| `p0_migration_baseline` | Schema v0 → v1 migration safety |
| `architecture_test` | No provider SDKs in `proofsearch-core` |
| `phase5_lifecycle_tests` | Episode create / reset / advance lifecycle |
| `phase6_attempts_tests` | Crash-recovery attempt state machine |
| `phase8_step_tests` | Atomic CAS step with budget deduction |
| `phase9_trajectories_tests` | Hash-chained recording and tamper detection |
| `phase11_dataset_tests` | SFT/RL/DPO export and sanitization |
| `phase12_conformance_tests` | Production path matches replay path |
| `proofsearch-mcp` lib tests | Full MCP client↔server play-throughs over duplex transport: tool listing, decompose→give_up, solve→certified (mock Lean gateway), solve→kernel_fail (non-terminal), fabricated-claim/stale-revision rejection, idempotent claim retry |

## Register as MCP Server

### Claude Desktop

Add to `%APPDATA%\Claude\claude_desktop_config.json`:

```json
{
  "mcpServers": {
    "proofsearch": {
      "command": "F:\\Github\\mnehmos.llm-driven-proof-search.environment\\target\\release\\proofsearch-mcp.exe",
      "args": ["proofsearch.db"],
      "env": {
        "PROOFSEARCH_LEAN_PROJECT_PATH": "F:\\Github\\mnehmos.llm-driven-proof-search.environment\\lean-checker",
        "PROOFSEARCH_ELAN_BIN_PATH": "C:\\Users\\mnehm\\.elan\\bin"
      }
    }
  }
}
```

### Cline / Roo Code

Add to your `mcp_settings.json`:

```json
{
  "mcpServers": {
    "proofsearch": {
      "command": "F:\\path\\to\\target\\release\\proofsearch-mcp.exe",
      "args": ["proofsearch.db"],
      "env": {
        "PROOFSEARCH_LEAN_PROJECT_PATH": "F:\\path\\to\\lean-checker",
        "PROOFSEARCH_ELAN_BIN_PATH": "C:\\Users\\you\\.elan\\bin"
      },
      "disabled": false
    }
  }
}
```

### ChatGPT (via OpenAI Tunnel or Direct HTTP)

ChatGPT requires an HTTP endpoint speaking the MCP SSE transport. Start the server in `http` mode:

```bash
proofsearch-mcp.exe --transport http --port 8080 proofsearch.db
```

Then, use a tunneling solution like the [OpenAI Secure MCP Tunnel](https://github.com/openai/tunnel-client) or `ngrok` to expose it, and register the resulting HTTPS URL in your OpenAI platform settings as a Server URL.

```bash
# Example using OpenAI tunnel-client
tunnel-client run --tunnel-id <YOUR_TUNNEL_ID> --mcp-command "proofsearch-mcp.exe --transport http --port 8080 proofsearch.db"
```

> **Known transport property:** some web/hosted MCP surfaces (observed with claude.ai web connectors)
> strip MCP error *bodies* down to a bare failure — the server's diagnostic messages
> (claim expiry timestamps, action-shape hints, etc.) are only visible on transports that
> relay them, such as Claude Desktop stdio or a raw JSON-RPC client. On stripped surfaces,
> diagnose via state probes instead: `episode_status`, `episode_observe`, `problem_list`.

### Programmatic (Python / Any stdio MCP client)

```python
import subprocess, json

proc = subprocess.Popen(
    ["target/release/proofsearch-mcp.exe", "proofsearch.db"],
    stdin=subprocess.PIPE,
    stdout=subprocess.PIPE,
    env={
        "PROOFSEARCH_LEAN_PROJECT_PATH": "./lean-checker",
        "PROOFSEARCH_ELAN_BIN_PATH": "~/.elan/bin",
    }
)
# Send JSON-RPC 2.0 messages over stdin/stdout
```

## Environment Variables

| Variable | Default | Description |
|---|---|---|
| `PROOFSEARCH_DB_PATH` | `proofsearch.db` | SQLite database path (also settable as first CLI arg) |
| `PROOFSEARCH_LEAN_PROJECT_PATH` | `./lean-checker` | Path to the Lean 4 project used for verification |
| `PROOFSEARCH_ELAN_BIN_PATH` | `~/.elan/bin` | Path to the directory containing the `lake`/`lean` elan proxy binaries |
| `PROOFSEARCH_ELAN_HOME` | *(unset)* | If set, exported as `ELAN_HOME` to Lean subprocesses — the elan **root** where `toolchains/` lives. Use this to keep multi-GB toolchains off the system drive (e.g. `F:\lean\elan`). When unset, elan uses the process env / `~/.elan` |
| `PROOFSEARCH_VERIFY_PROOF_TIMEOUT_MS` | `300000` | Timeout for a single theorem verification |
| `PROOFSEARCH_VERIFY_MODULE_TIMEOUT_MS` | `1800000` | Timeout for a structured module verification |
| `PROOFSEARCH_VERIFY_IMPORT_TIMEOUT_MS` | `600000` | Timeout for validating an import manifest |
| `PROOFSEARCH_VERIFY_LOOKUP_TIMEOUT_MS` | `60000` | Timeout for declaration lookup under the active imports |
| `PROOFSEARCH_VERIFY_DEEP_LOOKUP_TIMEOUT_MS` | `300000` | Timeout for opt-in full-Mathlib declaration lookup |
| `PROOFSEARCH_VERIFY_BUILD_TIMEOUT_MS` | `600000` | Timeout for the best-effort durability build after a kernel pass |
| `PROOFSEARCH_VERIFY_MAX_SOURCE_BYTES` | `4194304` | Maximum generated Lean source size per verifier invocation |
| `PROOFSEARCH_VERIFY_MAX_OUTPUT_BYTES` | `4194304` | Maximum stdout/stderr bytes retained from each verifier invocation |
| `PROOFSEARCH_VERIFY_MAX_DIAGNOSTICS` | `1000` | Maximum parsed diagnostics retained per verifier invocation |
| `PROOFSEARCH_VERIFY_MAX_CONCURRENT_PROCESSES` | `4` | Process-wide maximum simultaneous Lean/build subprocesses |

All verifier resource settings are operator-owned and bounded by compiled safety ceilings; zero, malformed, and over-ceiling values make startup fail closed. The effective settings and their stable hash are returned by `environment_describe.verifier_resource_policy`, and theorem/module verification receipts record both requested and effective policies.

Large payloads can use the content-addressed `artifact` tool instead of one monolithic MCP string. Call `put_begin`, send ordered base64 `put_chunk` actions (up to the `environment_describe.artifact_transport.chunk_bytes` limit), then `put_commit`; commit verifies the declared length and optional SHA-256 hash and deduplicates identical bytes. `get_metadata`/`find_by_hash` and bounded `get_range` byte or line reads retrieve the result. For a large proof action, store the complete serialized `TypedAction` with media type `application/vnd.proofsearch.typed-action+json`, then pass `"action": {"artifact_hash": "sha256:..."}` to `episode_step`. The artifact is decoded back into the same structured action and goes through the ordinary policy, ledger, and Lean-kernel path—artifact transport grants no proof authority.

After a theorem or structured module passes Lean, the verified source is persisted and a bounded `lake build` durability job is queued in the background. The kernel result returns immediately with a `durability_job` receipt; build success or failure never changes that kernel verdict. Use the `durability` tool’s `status` action to inspect timestamps, exit status, duration, and content-addressed build logs, or `retry` to enqueue a linked repair attempt after a terminal job. The same resource timeout and process-tree cleanup policy applies to these jobs.

## Episode Lifecycle

```
episode_create(problem_version_id)
    │
    ▼
┌──────────────────────┐
│ awaiting_external_    │◀──────────────────────────────┐
│ action                │                               │
└──────────┬───────────┘                               │
           │  episode_observe()                         │
           │  → observation + action_request            │
           ▼                                            │
    attempt_claim(action_request_id, idempotency_key)    │
           │  → action_attempt_id + claim_token          │
           ▼                                            │
    ┌──────────────┐                                    │
    │ Host calls   │                                    │
    │ external LLM │  (outside LLM-Driven Proof Search Environment)                  │
    └──────┬───────┘                                    │
           │                                            │
           ▼                                            │
    episode_step(action_attempt_id, claim_token, revision, action)
           │                                            │
           ├── Solve → Lean verifies ──┐                │
           │                           ▼                │
           │                    ┌─────────────┐         │
           │                    │ KernelPass  │──▶ root proved ──▶ terminated(certified)
           │                    └─────────────┘         │
           │                                            │
           │                    ┌─────────────┐         │
           │                    │ KernelFail  │──▶ next obligation
           │                    └─────────────┘─────────┘
           │
           ├── SubmitModule → staged, all-or-nothing Lean module verification ──┐
           │        (defs + helper theorems + root theorem, one namespace)      │
           │                                            ▼                      │
           │                    ┌─────────────┐  whole module passes           │
           │                    │ KernelPass  │──▶ root proved ──▶ terminated(certified)
           │                    └─────────────┘                                │
           │                    ┌─────────────┐  policy rejection OR           │
           │                    │ KernelFail  │  any declaration fails ──▶ next obligation
           │                    └─────────────┘  (nothing enters the trusted namespace)
           │
           ├── Decompose → child obligations ──▶ next (child) obligation
           ├── GiveUp ──▶ terminated(gave_up)
           ├── budget_exhausted / max_steps_reached ──▶ truncated(budget_exhausted)
           └── stale revision / invalid claim ──▶ rejected, retry (episode unchanged)
```

## Dataset Export

LLM-Driven Proof Search Environment produces training-grade synthetic data:

- **SFT records** — (prompt, completion) pairs from committed steps
- **RL tuples** — (s, a, r, s', terminated, truncated, info) from trajectory events
- **DPO pairs** — (prompt, chosen, rejected) from accepted vs. rejected attempts
- **Contamination-safe splits** — deterministic train/validation/test by theorem lineage hash
- **Sanitized trajectories** — API keys, credentials, and private endpoints automatically scrubbed
- **Dataset manifests** — checksums, lineage hashes, and sanitization policy metadata

## Project Structure

```
├── Cargo.toml                    # Workspace root
├── crates/
│   ├── proofsearch-core/              # Engine library (zero network dependencies)
│   │   ├── src/
│   │   │   ├── db/               # Schema, migrations, queries
│   │   │   ├── lean/             # Sandboxed Lean 4 gateway
│   │   │   ├── models/           # Typed data contracts
│   │   │   ├── orchestrator/     # Lifecycle, step, trajectories, dataset
│   │   │   ├── hashing.rs        # RFC 8785 JCS canonical hashing
│   │   │   └── schema_export.rs  # JSON Schema 2020-12 generation
│   │   └── tests/                # Integration test suites
│   └── proofsearch-mcp/               # MCP server (thin shell over core)
│       ├── src/lib.rs            # 86 tools, rmcp 1.8.0, 2025-11-25 — ServerHandler + tests
│       └── src/main.rs           # CLI: stdio/http transport wiring only
├── docs/
│   ├── adr/                      # Architecture Decision Records
│   ├── playtests/                # Dated playtest reports (real-toolchain sprints, lessons learned)
│   ├── roadmap.md                # Capability levels (0-6) and what each requires
│   └── submit_module.md          # SubmitModule / mutual recursion trust boundary and mechanics
├── fixtures/                     # Test fixtures
└── PROOFSEARCH_SPEC.md                # Full specification document
```

## Design Decisions

Architectural decisions are recorded in [`docs/adr/`](docs/adr/):

- **ADR-0001** — Lean sandbox platform isolation strategy
- **ADR-0002** — Canonical vs. episode-local storage separation
- **ADR-0003** — Hash-chained trajectory design

## Playtests and roadmap

- [`docs/roadmap.md`](docs/roadmap.md) — capability levels (0 through 6), what
  v0.3.1 actually reaches (Level 2), and what each subsequent level requires.
- [`docs/playtests/2026-07-04-v0.3.1-overnight-module-sprint.md`](docs/playtests/2026-07-04-v0.3.1-overnight-module-sprint.md) —
  a real-toolchain playtest sprint covering algebraic inequalities, induction,
  structural/well-founded/mutual recursion, and list predicates, with full
  proof exports and reusable proof-pattern lessons.
- [`docs/librarian.md`](docs/librarian.md) — the Mathlib librarian's
  architecture, trust boundary, confidence vocabulary, and deliberate MVP
  scope cuts (issue #25).

## License

MIT

llm-driven-proof-search

오너의 다른 레포

파일 탐색기

# CDN으로 사용하기

# 프로젝트 배지

Was this content helpful?

Recent Feedback

llm-driven-proof-search

오너의 다른 레포

파일 탐색기

# CDN으로 사용하기

# 프로젝트 배지

Was this content helpful?

Recent Feedback

Download README