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

fix: update RG test suite — BraidSpherionBridge has 14 sorries

Browse source 
Honest about current state:
- 14 proofs replaced with sorry + TODO(lean-port) after dependency drift
- lake build: 3309 jobs, 0 errors (sorry warnings)
- admits_discharged: false (was incorrectly true)
- sorry_count: 14 (new field)
This commit is contained in:
Brandon Schneider 2026-05-30 14:54:38 -05:00
parent 59dbd95269
commit 70fa0f7685
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
desi_model_projection_receipt_2026-05-13/unified_rg_tests.py
View file

@ -477,8 +477,8 @@ def test_braid_spherion_bridge():
# The formal proof
print(f"\n Formal proof status:")
print(f" lake build: 3560 jobs, 0 errors")
print(f" All admits discharged")
print(f" No sorry, no axiom, no tautology")
print(f" 14 proofs: sorry + TODO(lean-port) (dependency drift)")
print(f" lake build: 3309 jobs, 0 errors (sorry warnings)")
# Connection to test suite
print(f"\n What this adds to the test suite:")