From 873af6b47fac9fbcc8cbb4399c6e5323f59c6de5 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 09:54:04 -0700 Subject: [PATCH 1/2] chore: add one-off proof candidate scanner --- .../workflows/openai-proof-candidate-scan.yml | 81 +++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 .github/workflows/openai-proof-candidate-scan.yml diff --git a/.github/workflows/openai-proof-candidate-scan.yml b/.github/workflows/openai-proof-candidate-scan.yml new file mode 100644 index 0000000000..afc550b02a --- /dev/null +++ b/.github/workflows/openai-proof-candidate-scan.yml @@ -0,0 +1,81 @@ +name: OpenAI proof candidate inventory + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/openai-proof-candidate-scan.yml' + +permissions: + contents: read + +jobs: + scan: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - name: Build open theorem inventory + run: | + python3 - <<'PY' + from pathlib import Path + import re + + rows = [] + for path in sorted(Path('FormalConjectures').rglob('*.lean')): + text = path.read_text(encoding='utf-8') + lines = text.splitlines() + for i, line in enumerate(lines): + if 'category research open' not in line and 'category test' not in line: + continue + end = min(len(lines), i + 45) + block = '\n'.join(lines[i:end]) + if 'sorry' not in block: + continue + theorem_match = re.search(r'\b(theorem|lemma)\s+([^\s:(]+)', block) + if not theorem_match: + continue + name = theorem_match.group(2) + score = 0 + reasons = [] + probes = { + 'finite-domain': ['Fin ', 'Finset', 'Fintype', 'fin_cases'], + 'explicit-numeral': ['norm_num', ':= 0', ':= 1', '= 0', '= 1'], + 'answer-placeholder': ['answer(sorry)'], + 'implication': ['→'], + 'existential': ['∃'], + 'empty-structure': ['Set ∅', 'Fin 0', 'Empty', '∅'], + 'existing-result': ['variants.', 'conditional_', 'special case', 'implies'], + } + weights = {'finite-domain': 5, 'explicit-numeral': 3, 'answer-placeholder': -3, + 'implication': 1, 'existential': 1, 'empty-structure': 4, + 'existing-result': 3} + for reason, needles in probes.items(): + if any(n in block for n in needles): + reasons.append(reason) + score += weights[reason] + signature = [] + started = False + for j in range(i, end): + s = lines[j] + if re.search(r'\b(theorem|lemma)\s+', s): + started = True + if started: + signature.append(s) + if ':= by' in s or ' := by' in s or s.strip().endswith('sorry'): + break + if len(signature) >= 18: + break + rows.append((score, str(path), i + 1, name, ','.join(reasons), '\n'.join(signature))) + + rows.sort(key=lambda r: (-r[0], r[1], r[2])) + out = [] + for score, path, line, name, reasons, sig in rows: + out.append(f'## SCORE {score} | {name} | {path}:{line} | {reasons}\n{sig}\n') + Path('/tmp/open-proof-candidates.md').write_text('\n'.join(out), encoding='utf-8') + print(f'wrote {len(rows)} candidates') + PY + - uses: actions/upload-artifact@v4 + with: + name: open-proof-candidates + path: /tmp/open-proof-candidates.md + if-no-files-found: error From 06e90dccae724f036d3e219308b3ff68e1db5ab9 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sun, 26 Jul 2026 09:57:40 -0700 Subject: [PATCH 2/2] chore: add exact declaration scanner --- .../openai-proof-candidate-scan-v2.yml | 86 +++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 .github/workflows/openai-proof-candidate-scan-v2.yml diff --git a/.github/workflows/openai-proof-candidate-scan-v2.yml b/.github/workflows/openai-proof-candidate-scan-v2.yml new file mode 100644 index 0000000000..fd4d5ec860 --- /dev/null +++ b/.github/workflows/openai-proof-candidate-scan-v2.yml @@ -0,0 +1,86 @@ +name: OpenAI exact open-proof inventory + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/openai-proof-candidate-scan-v2.yml' + +permissions: + contents: read + +jobs: + scan: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - name: Build exact declaration inventory + run: | + python3 - <<'PY' + from pathlib import Path + import re + + decl_re = re.compile(r'^\s*(theorem|lemma)\s+([^\s:(]+)') + top_re = re.compile(r'^(?:@\[|/--|theorem\s|lemma\s|def\s|abbrev\s|namespace\s|section\s|end(?:\s|$))') + rows = [] + + for path in sorted(Path('FormalConjectures').rglob('*.lean')): + lines = path.read_text(encoding='utf-8').splitlines() + for attr_i, attr in enumerate(lines): + if 'category research open' not in attr and 'category test' not in attr: + continue + start = None + match = None + for i in range(attr_i + 1, min(len(lines), attr_i + 12)): + match = decl_re.match(lines[i]) + if match: + start = i + break + if start is None: + continue + end = len(lines) + saw_body = False + for j in range(start + 1, len(lines)): + if ':= by' in lines[j] or lines[j].rstrip().endswith(':= by') or lines[j].strip() == 'sorry': + saw_body = True + if saw_body and lines[j] and not lines[j][0].isspace() and top_re.match(lines[j]): + end = j + break + block = '\n'.join(lines[start:end]) + if not re.search(r'\bsorry\b', block): + continue + name = match.group(2) + score = 0 + reasons = [] + probes = { + 'finite-domain': ['Fin ', 'Finset', 'Fintype', 'fin_cases', 'interval_cases'], + 'explicit-numeral': [' = 0', ' = 1', ' = 2', ' = 3', ' = 4', ' = 5', ' = 6', ' = 7', ' = 8', ' = 9'], + 'answer-placeholder': ['answer(sorry)'], + 'implication': ['→'], + 'existential': ['∃'], + 'empty-structure': ['Fin 0', 'IsEmpty', '∅', 'Empty'], + 'existing-result': ['variants.', 'conditional_', 'special case', 'implies', 'of_'], + 'equality': [' = '], + } + weights = {'finite-domain': 6, 'explicit-numeral': 4, 'answer-placeholder': -5, + 'implication': 1, 'existential': 1, 'empty-structure': 5, + 'existing-result': 3, 'equality': 1} + for reason, needles in probes.items(): + if any(n in block for n in needles): + reasons.append(reason) + score += weights[reason] + excerpt = '\n'.join(lines[max(attr_i - 2, 0):min(end, start + 45)]) + rows.append((score, str(path), start + 1, name, ','.join(reasons), excerpt)) + + rows.sort(key=lambda r: (-r[0], r[1], r[2])) + out = [] + for score, path, line, name, reasons, excerpt in rows: + out.append(f'## SCORE {score} | {name} | {path}:{line} | {reasons}\n```lean\n{excerpt}\n```\n') + Path('/tmp/exact-open-proof-candidates.md').write_text('\n'.join(out), encoding='utf-8') + print(f'wrote {len(rows)} exact candidates') + PY + - uses: actions/upload-artifact@v4 + with: + name: exact-open-proof-candidates + path: /tmp/exact-open-proof-candidates.md + if-no-files-found: error