allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/shared-data/proof_traces
History
Brandon Schneider 31890cf3e9 feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 
- 24/24 processed, 0 errors (12 verified, 12 failed)
- Average 2.0 steps per proof (max 5 steps)
- 11 tactic families detected
- Verified proofs: avg gap=2.50 vs Failed: avg gap=1.50
- proof_traces/*.trace.json + *.decomp.json stored per theorem
2026-05-26 02:37:22 -05:00
..
canary_apply_chain.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_apply_chain.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_calc_chain.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_calc_chain.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_cases_and_elim.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_cases_and_elim.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_cases_or_swap.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_cases_or_swap.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_constructor_example.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_constructor_example.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_bad_coercion.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_bad_coercion.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_missing_lemma.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_missing_lemma.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_type_mismatch.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_type_mismatch.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_unsat.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_fail_unsat.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_have_chain.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_have_chain.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_add_succ.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_add_succ.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_add_zero.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_add_zero.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_factorial.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_factorial.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_mul_zero.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_induct_mul_zero.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_intro_all.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_intro_all.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_intro_apply.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_intro_apply.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_chain_ineq.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_chain_ineq.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_chain_unsat.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_chain_unsat.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_distrib.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_distrib.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_reorder_sum.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_omega_reorder_sum.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_3step.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_3step.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_eq.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_eq.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_mixed.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_chain_mixed.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_then_omega.decomp.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_rw_then_omega.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00
canary_simp_chain_simple.trace.json feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 2026-05-26 02:37:22 -05:00