Skip to content

Audit the Erdős 625 manuscript line by line and theorem by theorem #52

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
SamPetkov wants to merge 8 commits into
base: agent/625-sharp-deficit-product-exposition
Choose a base branch
from
Draft

Audit the Erdős 625 manuscript line by line and theorem by theorem #52

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
0830c9f
Add deterministic canonical-TeX source map extractor
SamPetkov Jul 27, 2026
16f49fa
Add machine-readable theorem and claim status manifest
SamPetkov Jul 27, 2026
762ef2c
Add literal line-by-line and theorem-by-theorem mathematical audit
SamPetkov Jul 27, 2026
09787b9
Add deterministic audit coverage and status checker
SamPetkov Jul 27, 2026
1069946
Validate literal theorem audit through active Section 8 workflow
SamPetkov Jul 27, 2026
65cfd74
Validate theorem identifiers rather than full parenthetical headings
SamPetkov Jul 27, 2026
9b3057f
Preserve audit checker logs on validation failure
SamPetkov Jul 27, 2026
619f4cc
Remove cosmetic phrase gate from literal audit checker
SamPetkov Jul 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 51 additions & 0 deletions .github/workflows/erdos625-sharp-deficit-product.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,12 @@ on:
- "625/formalization/Erdos625/Section8ThreeQuarterDeficitArithmetic.lean"
- "625/proofs/SECTION8_SHARP_DEFICIT_PRODUCT_AND_REWRITE.md"
- "625/arxiv/SECTION8_SHARP_DEFICIT_INSERT_V2.tex"
- "625/arxiv/main.tex"
- "625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md"
- "625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json"
- "625/experiments/section8_sharp_deficit_product.py"
- "625/experiments/extract_line_by_line_audit_map.py"
- "625/experiments/check_line_by_line_audit.py"
- ".github/workflows/erdos625-sharp-deficit-product.yml"
workflow_dispatch:

Expand Down Expand Up @@ -102,3 +107,49 @@ jobs:
name: erdos625-sharp-deficit-product-log
path: /tmp/erdos625-sharp-deficit-product.log
if-no-files-found: ignore

line-by-line-theorem-audit:
runs-on: ubuntu-24.04
steps:
- uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
- name: Compile audit tools
run: |
python -m py_compile 625/experiments/extract_line_by_line_audit_map.py
python -m py_compile 625/experiments/check_line_by_line_audit.py
- name: Run audit consistency checker
id: audit-check
continue-on-error: true
shell: bash
run: |
set +e
python 625/experiments/check_line_by_line_audit.py \
> /tmp/erdos625-line-audit-check.log 2>&1
status=$?
cat /tmp/erdos625-line-audit-check.log
exit $status
- name: Upload audit checker log
if: always()
uses: actions/upload-artifact@v4
with:
name: erdos625-line-audit-check-log
path: /tmp/erdos625-line-audit-check.log
if-no-files-found: error
- name: Run audit checker with optimization
if: steps.audit-check.outcome == 'success'
run: python -O 625/experiments/check_line_by_line_audit.py
- name: Generate exact source-map artifact
if: steps.audit-check.outcome == 'success'
run: |
python 625/experiments/extract_line_by_line_audit_map.py \
625/arxiv/main.tex \
--output /tmp/ERDOS625_GENERATED_SOURCE_MAP.md
- name: Upload generated source map
if: steps.audit-check.outcome == 'success'
uses: actions/upload-artifact@v4
with:
name: erdos625-generated-source-map
path: /tmp/ERDOS625_GENERATED_SOURCE_MAP.md
if-no-files-found: error
- name: Fail if audit checker failed
if: steps.audit-check.outcome == 'failure'
run: exit 1
Loading
Loading