User:DrDisentangle/BB6 formal proofs: Difference between revisions
Jump to navigation
Jump to search
Created page with "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. {| class="wikitable" |- ! Machine !! Rules Proved !! Math Derived !! H/NH Proof attempt !! Final Proof |- | 1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB || || || || |- | 1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC || || || || |- | 1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---..." |
No edit summary |
||
| Line 3: | Line 3: | ||
{| class="wikitable" | {| class="wikitable" | ||
|- | |- | ||
! Machine !! Rules Proved !! Math Derived !! H/NH Proof attempt !! Final Proof | ! Machine !! Rules Proved !! Math Derived !! Prob. Model !! H/NH Proof attempt !! Final Proof | ||
|- | |- | ||
| [[1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB]] || || || || | | [[1RB1LD_1RC0LE_1LA1RE_0LF1LA_1RB0RB_---0LB]] || - || || || || | ||
|- | |- | ||
| [[1RB0RB_1LC1RE_1LF0LD_1RA1LD_1RC1RB_---1LC]] || || || || | | [[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] || || | ||
|- | |- | ||
| [[1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE]] || || || || | | [[1RB1LA_0LC0RC_1LE1RD_1RE1RC_1LF0LA_---1LE]] || - || || || | ||
|- | |- | ||
| [[1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA]] || || || || | | [[1RB1RC_1LC1LE_1RA1RD_0RF0RE_1LA0LB_---1RA]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/AntiHydra2.v R] || || || | ||
|- | |- | ||
| [[1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---]] || || || || | | [[1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1RC1RF_1LA0RA_0LA0LE_1LD1LA_0RB---.v R] || || || || | ||
|- | |- | ||
| [[1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA]] || || || || | | [[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] || || | ||
|- | |- | ||
| [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || || || || | | [[1RB0RD_0RC1RE_1RD0LA_1LE1LC_1RF0LD_---0RA]] || || || || | ||
| Line 35: | Line 35: | ||
| [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || || || || | | [[1RB0LC_0LC0RF_1RD1LC_0RA1LE_---0LD_1LF1LA]] || || || || | ||
|- | |- | ||
| [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || || || || | | [[1RB1LD_1RC1RE_0LA1LB_0LD1LC_1RF0RA_---0RC]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB1LD%201RC1RE%200LA1LB%200LD1LC%201RF0RA%20---0RC.v R] || || || || | ||
|- | |- | ||
| [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || || || || | | [[1RB0LB_1LC0RE_1LA1LD_0LC---_0RB0RF_1RE1RB]] || [https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LB%201LC0RE%201LA1LD%200LC---%200RB0RF%201RE1RB.v R] || || || | ||
|- | |- | ||
| [[1RB1LE_0LC0LB_1RD1LC_1RD1RA_1RF0LA_---1RE]] || || || || | | [[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] || || || || | |||
|- | |||
|} | |} | ||
Revision as of 09:38, 19 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.