allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: CRTSidonN auto-generated, ~15 structural issues — documenting TODO

Browse source 
The pipeline-math template (5-file frozen pattern, linear_combination tactics,
decide for residue checks, lcoeff-descent for quotient witnesses) is now
documented in docs/frozen_template/. The auto-generated CRTSidonN.lean
needs manual porting to mathlib v4.30.0-rc2 API.

Adopted refinements:
- verify_lean.py: 5-check pipeline (SHA pins, banned keywords, build, axioms, discharge)
- prove.py: 5-check pipeline for LLM proof filling
- docs/frozen_template/: reusable Defs/Theorems/Proofs/Discharge/Solution pattern
This commit is contained in:
allaun 2026-07-04 10:28:25 -05:00
parent 1b5d57bed3
commit ae55a78627
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lakefile.lean
View file

@ -47,7 +47,7 @@ lean_lib «SilverSightFormal» where
`CoreFormalism.HopfFibration, `CoreFormalism.HopfFibration,
`CoreFormalism.StrandCapacityBound, `CoreFormalism.StrandCapacityBound,
`CoreFormalism.CRTSidon, `CoreFormalism.CRTSidon,
-- `CoreFormalism.CRTSidonN, -- TODO(lean-port): auto-generated, targets different mathlib API -- `CoreFormalism.CRTSidonN, -- TODO(lean-port): auto-generated, ~15 structural issues
`SilverSight.AngrySphinx, `SilverSight.AngrySphinx,
`SilverSight.CollatzBraid, `SilverSight.CollatzBraid,
`SilverSight.GoldenSpiral, `SilverSight.GoldenSpiral,