An unreleased version of Claude found an improved lower bound for the length of the minimum superpermutation on seven symbols: https://github.com/jlebar/superperm7-ge-5898

I can't speak to the quality of the formalisation, but the exposition is *dramatically* better than those we've seen from current frontier models in the last couple of weeks.