User:DrDisentangle/BB6 formal proofs: Difference between revisions

From BusyBeaverWiki
Jump to navigation Jump to search
← Older editNewer edit →
VisualWikitext
No edit summary
No edit summary
Line 3: Line 3:
{| class="wikitable"
{| class="wikitable"
|-
|-
! Machine !! Rules Proved !! Math Derived !! Prob. Model !! H/NH Proof attempt !! Final Proof
! Machine !! Rules Proved !! Math Derived !! BMO !! Prob. Model !! H/NH Proof attempt !! Final Proof
|-
|-
| [[1RB1RE 1LC0RA 0RD1LB ---1RC 1LF1RE 0LB0LE]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RE%201LC0RA%200RD1LB%20---1RC%201LF1RE%200LB0LE L] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RE%201LC0RA%200RD1LB%20---1RC%201LF1RE%200LB0LE L] || || ||
| [[1RB1RE 1LC0RA 0RD1LB ---1RC 1LF1RE 0LB0LE]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RE%201LC0RA%200RD1LB%20---1RC%201LF1RE%200LB0LE L] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RE%201LC0RA%200RD1LB%20---1RC%201LF1RE%200LB0LE L] || #1 || || ||
|-
|-
| [[1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra.v R] [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || ||
| [[1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra.v R] [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || #2 || [https://github.com/rwst/bbchallenge/tree/main/Antihydra L] || ||
|-
|-
| [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RD%200RC1RE%201RD0LA%201LE1LC%201RF0LD%20---0RA/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RD%200RC1RE%201RD0LA%201LE1LC%201RF0LD%20---0RA/machine.lean L] || || ||
| [[1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v R] || || #5 || || ||
|-
|-
| [[1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RA%200RC1RC%201LD0LF%200LE1LE%201RA0LB%20---0LC/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RA%200RC1RC%201LD0LF%200LE1LE%201RA0LB%20---0LC/machine.lean L] || || ||
| [[1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD]] || - || || #6 || || ||
|-
|-
| [[1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0RB%201LC1RE%201LF0LD%201RA1LD%201RC1RB%20---1LC.v R] [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] || ||
| [[1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA]] || - || || #8 || || ||
|-
|-
| [[1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LA%200LC0RC%201LE1RD%201RE1RC%201LF0LA%20---1LE/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LA%200LC0RC%201LE1RD%201RE1RC%201LF0LA%20---1LE/machine.lean L] || ||
| [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RD%200RC1RE%201RD0LA%201LE1LC%201RF0LD%20---0RA/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RD%200RC1RE%201RD0LA%201LE1LC%201RF0LD%20---0RA/machine.lean L] || || || ||
|-
|-
| [[1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra2.v R] || || ||
| [[1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RA%200RC1RC%201LD0LF%200LE1LE%201RA0LB%20---0LC/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RA%200RC1RC%201LD0LF%200LE1LE%201RA0LB%20---0LC/machine.lean L] || || || ||
|-
|-
| [[1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---.v R] || || || ||
| [[1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0RB%201LC1RE%201LF0LD%201RA1LD%201RC1RB%20---1LC.v R] [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] ||| [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] || || [https://github.com/rwst/bbchallenge/blob/main/1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC/ L] || ||
|-
|-
| [[1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA]] || - || || || ||
| [[1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LA%200LC0RC%201LE1RD%201RE1RC%201LF0LA%20---1LE/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LA%200LC0RC%201LE1RD%201RE1RC%201LF0LA%20---1LE/machine.lean L] || || || ||
|-
|-
| [[1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0RE%201LC0RA%201LA1LD%201LC1LF%200LC0LB%201LE---.lean L] || || || ||
| [[1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra2.v R] || || || || ||
|-
|-
| [[1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0LD%201RC1RA%201LD0RB%201LE1LA%201RF0RC%20---1RE.lean L] || || || ||
| [[1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---.v R] || || || || ||
|-
|-
| [[1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RE%201LC1LD%200RA0LD%201LB0LA%201RF1RA%20---1LB/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RE%201LC1LD%200RA0LD%201LB0LA%201RF1RA%20---1LB/machine.lean L] || || ||
| [[1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA]] || - || || || || ||
|-
|-
| [[1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF]] || - || || || ||
| [[1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE---]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0RE%201LC0RA%201LA1LD%201LC1LF%200LC0LB%201LE---.lean L] || || || || ||
|-
|-
| [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || - || || || ||
| [[1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE]] || [https://github.com/int-y1/proofs/blob/1929f57df4dd7afcc11c3f458e20526fd1f991e0/BusyLean/Individual/1RB0LD%201RC1RA%201LD0RB%201LE1LA%201RF0RC%20---1RE.lean L] || || || || ||
|-
|-
| [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD%201RC1RE%200LA1LB%200LD1LC%201RF0RA%20---0RC.v R] || || || ||
| [[1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RE%201LC1LD%200RA0LD%201LB0LA%201RF1RA%20---1LB/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB0RE%201LC1LD%200RA0LD%201LB0LA%201RF1RA%20---1LB/machine.lean L] || || || ||
|-
|-
| [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB%201LC0RE%201LA1LD%200LC---%200RB0RF%201RE1RB.v R] || || ||
| [[1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RE%201LC1LD%20---1LA%201LB1LE%200RF0RA%201LD1RF/machine.lean L] || [https://github.com/rwst/bbchallenge/blob/main/1RB1RE%201LC1LD%20---1LA%201LB1LE%200RF0RA%201LD1RF/machine.lean L] || || || ||
|-
|-
| [[1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE]] || - || || || ||
| [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || - || || || || ||
|-
|-
| [[1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA]] || - || || || ||
| [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD%201RC1RE%200LA1LB%200LD1LC%201RF0RA%20---0RC.v R] || || || || ||
|-
|-
| c [[1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0LC%201LC0RD%201LF1LA%201LB1RE%201RB1LE%20---0LE/machine.lean *L] || || || ||
| [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB%201LC0RE%201LA1LD%200LC---%200RB0RF%201RE1RB.v R] || || || || ||
|-
|-
| c [[1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LD%201RC0LE%201LA1RE%200LF1LA%201RB0RB%20---0LB/machine.lean *L] || || || ||
| [[1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE]] || - || || || || || ||
|-
|-
| c [[1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v R] || || || ||
| c [[1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE]] || [https://github.com/rwst/bbchallenge/blob/main/1RB0LC%201LC0RD%201LF1LA%201LB1RE%201RB1LE%20---0LE/machine.lean *L] || || || || ||
|-
|-
| c [[1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1LA%201RC0RF%201RD---%200LE1RB%20---0LA%201LD1RF L] || || || [https://github.com/rwst/bbchallenge/tree/main/1RB1LA%201RC0RF%201RD---%200LE1RB%20---0LA%201LD1RF L] ||
| c [[1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB]] || [https://github.com/rwst/bbchallenge/blob/main/1RB1LD%201RC0LE%201LA1RE%200LF1LA%201RB0RB%20---0LB/machine.lean *L] || || || || ||
|-
|-
| c [[1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RF%201LC1LF%200RE1LD%200LB1LD%20---1RC%201RA0RD *L] || || || ||
| c [[1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1LA%201RC0RF%201RD---%200LE1RB%20---0LA%201LD1RF L] || || || || [https://github.com/rwst/bbchallenge/tree/main/1RB1LA%201RC0RF%201RD---%200LE1RB%20---0LA%201LD1RF L] ||
|-
|-
| c [[1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE]] || - || || || ||
| c [[1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD]] || [https://github.com/rwst/bbchallenge/tree/main/1RB1RF%201LC1LF%200RE1LD%200LB1LD%20---1RC%201RA0RD *L] || || || || ||
|-
| c [[1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE]] || - || || || || ||
|-
|-
|}
|}


(*) incomplete
(*) incomplete

Revision as of 07:33, 26 April 2026

This page is a draft of something to be added to BB(6). The goal is to keep track of which BB(6) cryptids (or candidates) have Rocq/Lean proofs of specific stages up to halting/nonhalting proofs.

Machine Rules Proved Math Derived BMO Prob. Model H/NH Proof attempt Final Proof
1RB1RE 1LC0RA 0RD1LB ---1RC 1LF1RE 0LB0LE L L #1
1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA R L L #2 L
1RB0LD 1LC0RA 1RA1LB 1LA1LE 1RF0LC ---0RE R #5
1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD - #6
1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA - #8
1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA L L
1RB1RA_0RC1RC_1LD0LF_0LE1LE_1RA0LB_---0LC L L
1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC R L L L
1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE L L
1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA R
1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB--- R
1RB---_0RC0RE_1RD1RF_1LE0LB_1RC0LD_1RC1RA -
1RB0RE_1LC0RA_1LA1LD_1LC1LF_0LC0LB_1LE--- L
1RB0LD_1RC1RA_1LD0RB_1LE1LA_1RF0RC_---1RE L
1RB0RE_1LC1LD_0RA0LD_1LB0LA_1RF1RA_---1LB L L
1RB1RE_1LC1LD_---1LA_1LB1LE_0RF0RA_1LD1RF L L
1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA -
1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC R
1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB R
1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE -
c 1RB0LC_1LC0RD_1LF1LA_1LB1RE_1RB1LE_---0LE *L
c 1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB *L
c 1RB1LA 1RC0RF 1RD--- 0LE1RB ---0LA 1LD1RF L L
c 1RB1RF_1LC1LF_0RE1LD_0LB1LD_---1RC_1RA0RD *L
c 1RB---_0RC0RD_1LD1RB_0LE0LC_1RA0LF_1LD1LE -

(*) incomplete

Retrieved from "https://wiki.bbchallenge.org/w/index.php?title=User:DrDisentangle/BB6_formal_proofs&oldid=7299"