Hasnain says:

“After learning Coq, mei began looking for an open problem to test it out. That’s when they found the Busy Beaver Challenge. A few weeks later, they’d translated several of the team’s proofs into Coq, including Ligocki and Kropitz’s proof that Skelet #1 never halts — Ligocki could finally be sure about it. Suddenly, an even higher standard of rigor than Stérin’s emphasis on reproducibility seemed possible. And it had all started with someone who had no formal training at all — an amateur mathematician.
“Let’s remember that means a lover of mathematics,” Moore said. “It is not a pejorative term.”

The Dam Breaks

Around the same time, a graduate student named Chris Xu made a breakthrough on the second monstrous machine — Skelet #17. It was usually easy to summarize the behavior of even the most fiendish five-rule Turing machines once you figured out how they worked. “Then you encounter some bullshit like Skelet 17, and you go, ‘Nah, the universe is trolling us,’” mei said. Understanding Skelet #17 by studying the patterns on its tape was like deciphering a secret message wrapped in four layers of encryption: Cracking one code just revealed another totally unrelated code, and two more below that. Xu had to decipher all of them before he could finally prove that the machine never halted.”

Posted on 2024-07-07T18:10:15+0000