Apparently, this is the proof in 19,000 lines of Coq: https://github.com/ccz1810...

		ks2048 on July 2, 2024 \| parent \| context \| favorite \| on: With fifth busy beaver, researchers approach compu... Apparently, this is the proof in 19,000 lines of Coq: https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v