Skip to content

feat(busy_beaver): Modularize Defs, port remaining 22 BB(6) Hard holdout cryptids, and register 735 theorems #29

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

Open
TomZahavy wants to merge 7 commits into
base: main
Choose a base branch
from
Open

feat(busy_beaver): Modularize Defs, port remaining 22 BB(6) Hard holdout cryptids, and register 735 theorems #29

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
29d0acf
Split BusyBeaver/Defs.lean into modular submodules with umbrella re-e…
Nov 6, 2026
1ace617
Add google3 predicates WordRun, Segmented, and IsCryptid with autoImp…
Nov 6, 2026
d67ecd7
Add tools/render_challenge.py, CI synchronization check, and regenera…
Nov 6, 2026
f281840
Add CORE_MANIFEST.json and tools/check_manifest.py with CI verification
Nov 6, 2026
0023bd8
Update BusyBeaver/README.md for modular Defs structure and goal predi…
Nov 6, 2026
eda142c
Port remaining 22 BB(6) Hard holdout cryptids and register in comparator
Nov 8, 2026
84cc3ba
Address PR #29 review feedback: tighten core defs, upgrade #424, expo…
Nov 11, 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
8 changes: 8 additions & 0 deletions .github/workflows/busy_beaver_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ on:
- 'lakefile.toml'
- 'lake-manifest.json'
- 'lean-toolchain'
- 'tools/**'
- 'CORE_MANIFEST.json'
- '.github/workflows/busy_beaver_ci.yml'
pull_request:
paths:
Expand All @@ -26,6 +28,8 @@ on:
- 'lakefile.toml'
- 'lake-manifest.json'
- 'lean-toolchain'
- 'tools/**'
- 'CORE_MANIFEST.json'
- '.github/workflows/busy_beaver_ci.yml'
workflow_dispatch:

Expand All @@ -45,6 +49,10 @@ jobs:
sudo sysctl -w kernel.apparmor_restrict_unprivileged_userns=0

- uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5
- name: Check BusyBeaverChallenge is synchronized with Defs
run: python3 tools/render_challenge.py --check
- name: Verify core manifest
run: python3 tools/check_manifest.py
- uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
with:
build-args: "BusyBeaver BusyBeaverChallenge"
Expand Down
24 changes: 24 additions & 0 deletions BusyBeaver.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ public import BusyBeaver.Cert
public import BusyBeaver.WordRLE
public import BusyBeaver.AffRLE
public import BusyBeaver.ElabRLE
public import BusyBeaver.Stack
public import BusyBeaver.WordRunStack
public import BusyBeaver.BB6.Equivalences
public import BusyBeaver.BB6.Hardness
public import BusyBeaver.BB6.HardnessEvidence
Expand Down Expand Up @@ -64,11 +66,33 @@ public import BusyBeaver.BB6.M_1RB1RD_1LC0RD_1RF1RB_1LE0RA_0LB0LE_HHH0RC
public import BusyBeaver.BB6.M_1RB1RE_1LC0RA_0RD1LB_HHH1RC_1LF1RE_0LB0LE
public import BusyBeaver.BB6.M_1RB1RE_1LC0RA_1RD0LB_1LB1RC_1LF0RD_HHH0LE
public import BusyBeaver.BB6.M_1RB1RE_1LC1LD_HHH1LA_1LB1LE_0RF0RA_1LD1RF
public import BusyBeaver.BB6.M_1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_HHH1RE
public import BusyBeaver.BB6.M_1RB1RF_0LC0RF_1RD1LC_HHH0LE_0RC1LF_1RA0LE
public import BusyBeaver.BB6.M_1RB1RF_1LC1LF_0RE1LD_0LB1LD_HHH1RC_1RA0RD
public import BusyBeaver.BB6.M_1RB1RF_1LCHHH_1LE1RD_1RA0RC_0LF0LA_0LD0RB
public import BusyBeaver.BB6.M_1RBHHH_1RC1LE_0RD0RF_0RE0LA_1LF0LB_1LA1LD
public import BusyBeaver.BB6.Accelerations.Stack
public import BusyBeaver.BB6.Accelerations.M_1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LA_0RC0RB_1LD1LA_1LC1RE_1RF0RD_1LCHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_0LC0RE_1LA0RD_0RB0LD_1RC1RF_1RAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_0LC0RE_1LA0RD_0RB0LF_1RC1LA_0RBHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LD_0RC1RD_1LA1RA_1LE0LE_1RF0LA_0RAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA0LF_0LC0RA_0REHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RA_0LBHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RA_0LEHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_0LAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_0LCHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_1LAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LE_1LC0RE_0RA0LD_1LA1LF_0LC0RE_1LEHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0RA_0LC0RE_1LE1LD_0LEHHH_1LF0LC_1RA1LE
public import BusyBeaver.BB6.Accelerations.M_1RB0RE_1LC1RA_1LD0LC_0RE0LA_1RA1RF_0RAHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0RE_1RCHHH_0RD0RC_1LE1LF_1LD1RA_1RC0LF
public import BusyBeaver.BB6.Accelerations.M_1RB0RF_1LCHHH_1LF1LD_1RE0LD_0RC0RE_1LC1RA
public import BusyBeaver.BB6.Accelerations.M_1RB0RF_1LCHHH_1RD0LC_0RE0RD_1LF1LC_1LE1RA
public import BusyBeaver.BB6.Accelerations.M_1RB1RF_1RC0RA_1LD1RB_1LE0LD_0RA0LB_0RBHHH
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_0RC0RB_1LD1LE_1LC1RF_1RB0LE_1RA0RD
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_1LC0RB_0LD0LC_1RE1RB_1RD1LF_1LA0LE
public import BusyBeaver.BB6.Accelerations.M_1RBHHH_1RC0LE_0LD0RF_1LB0RE_0RC0LE_1RD1RA
public import BusyBeaver.BB6.Accelerations.M_1RB0LB_0RC0LD_1LD1RE_0LA0RF_0RD1RF_0RCHHH
public import BusyBeaver.BB6.Accelerations.M_1RB0LC_1LC0RE_1LD1LC_1LA1RD_HHH0RF_0LB0RD
public import BusyBeaver.BB6.Accelerations.M_1RB0LC_1RC1RE_1LA0LD_0RB0RA_1RB1RF_1RDHHH
Expand Down
Loading
Loading