Snark conjecture is now finally a snark theorem

Recently I was asking about whether anyone could share the missing manuscript for apex cubic graph case of snark conjecture. Today a preprint appeared on arXiv that replaces this missing manuscript! Here - arxiv.org/abs/2608.22870 - written by another team, which is quite prolific in recent years in generalizing the 4 colour theorem in various directions. So, now someone needs to formalize the full proof in Rocq!