mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3f88b893a8
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)
18 lines
402 B
Text
18 lines
402 B
Text
/-
|
||
Copyright (c) 2026 SilverSight. All rights reserved.
|
||
Released under Apache 2.0 license.
|
||
|
||
Frozen theorem statements for [Module Name].
|
||
SHA-pinned after SETUP. `sorry` stubs are replaced by proofs in Proofs/.
|
||
-/
|
||
import ModuleName.Defs
|
||
|
||
/-! ## Main theorem -/
|
||
|
||
theorem my_theorem (x : ℕ) : x = x := by
|
||
sorry
|
||
|
||
/-! ## Auxiliary lemmas -/
|
||
|
||
lemma my_lemma (x y : ℕ) (h : x = y) : y = x := by
|
||
sorry
|