A second update on my previous posts https://mathstodon.xyz/@tao/115306424727150237 https://mathstodon.xyz/@tao/115316787727719049 on the #MathOverflow problem https://mathoverflow.net/questions/501066/is-the-least-common-multiple-sequence-textlcm1-2-dots-n-a-subset-of-t that had a first initial counterexample located with #AI assistance, and then the minimal counterexample obtained through a crowdsourced effort. As has happened with several previous projects, the crowdsourced effort has acquired a life of its own. In particular, the task of classifying *all* the counterexamples - which I had previously dismissed in my previous post as "somewhat tedious to perform", has in fact been completed, with the problem alternating between true and false for n between the first counterexample 71 and the last example 172, before settling down to a unending string of counterexamples. We now have some very efficient ways to either prove or disprove that a given number is highly abundant; some of the asymptotic analysis initially required some high powered number theory hypotheses such as the generalized Riemann hypothesis (GRH), but as our arguments became more efficient, this became unnecessary. We even have some recent contributions from the #LeanLang community, formalizing some of the counterexamples in Lean, almost in real-time! (1/3)