allaun 3f88b893a8 feat(autoresearch): 5-check verification pipeline + frozen theorem template ... Adapted from Peng et al. (2026) pipeline-math verify.sh: 1. SHA pin check — frozen theorem stubs pinned in frozen.sha256 2. Banned keywords — sorry/native_decide/admit blocked in proof files 3. lake build clean — 0 errors, 0 unexpected warnings 4. #print axioms — proof depends only on {propext, Class.choice, Quot.sound} 5. Discharge gate — @Frozen = @Proof := rfl (type-level gate) Frozen theorem template in docs/frozen_template/: Defs.lean — SHA-pinned definitions Theorems.lean — SHA-pinned sorry stubs Proofs/ — LLM fills these Discharge.lean — rfl discharge gate Solution.lean — clean exports verify_lean.py: standalone 5-check (no LLM)		2026-07-04 10:17:14 -05:00
..
Proofs	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
scripts	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
Defs.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
Discharge.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
lakefile.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
lean-toolchain	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
ModuleName.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
Solution.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00
Theorems.lean	feat(autoresearch): 5-check verification pipeline + frozen theorem template	2026-07-04 10:17:14 -05:00