3 ms·
Apparently, this is the proof in 19,000 lines of Coq: https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v https://github.com/ccz181078/Coq-BB5/blob/mai
by ks2048 2y ago
Apparently, this is the proof in 19,000 lines of Coq:
https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v