Post #1971035

Yet another stuff that will presented as a “mathematical breakthrough ” done by “autonomous AI”. In practice, a peripheral question nobody really cared about is indeed solved, that a weakly quasi-complete Noetherian local ring is in fact quasi-complete. The answer is negative, which just means that the intuition of its inventor was misled. And the “autonomous AI” is driven by a team of a dozen of people, built on 60 years of thinking about mechanization of mathematics, the 2 million human-written lines of code in the lean mathematical library mathlib, and several hundred of years of elaboration of modern mathematics. The creation of a counterexample made use of an auxiliary result which the authors of the paper (unironically) say “is very challenging to uncover without domain expertise”. In their paper, the mathematical construction is relegated to an appendix which says a lot about how they care about it. https://arxiv.org/html/2604.03789v1