i find this and other efforts from anthropic somewhat antisocial. technically they have achieved their goal, but in a way which does not benefit mathematics or humanity. Kevin Buzzards headline goal was to formalise FLT, but i’m sure the real aim was to create a formalised library of mathematics which is comprehensible to humans. By solving these famous problems by brute force, they are disincentivising the important work of making it digestible for everyone else, and so in my view this work in particular has negative societal value.