[1] https://publications.ias.edu/rpl/section/21 and https://publications.ias.edu/sites/default/files/letter-to-w... in particular
Unless it's been firmed up a great deal in recent times.
Predicts that special relativity holds up at all scales (check, according to all evidence so far), predicts general relativity at low energy scales (check).
So it's false that it has no testable predictions. None of this happened "in recent times" though, it's been understood for a long time.
Imagine if someone had said 30 years ago that the "higgs boson theory" is a failure because we couldn't then perform the experiments to detect it.
Don't get me wrong, I still regard string theory as a big success. It taught us a lot about mathematics and field theories in the last decades. However the predictive nature is basically non-existant so far.
In addition you haven't addressed the main point here which is that when some people say "can predict" they mean "in principle it can predict" whereas other mean "can predict today with currently available technological means". Regarding the former: yes it can. I already gave the example of one such prediction, but here's another one: all particles niches have stringy modes in their spectra. Regarding the later: maybe, but thats a problem with our technology, not with the theory.
I feel this conservation is going in circles already.
So you made your prediction only by choosing an axiom.
There is a reason that even some proponents of string theory call it the theory of anything.
I don't, thus neatly resolving your issue.
Neither does anybody else. Testable means something like testable today or in the designable future and it always has.
As for the fact this may mean a true theory is not testable today even though some hypothetical technology in the hypothetical future wielded by hypothetical beings could hypothetically resolve the problem, well, welcome to the universe we live in. This is not special pleading applied only to string theory. It's evenly applied to everything. It's just that string theory gets hit by this particularly hard, although not uniquely so (to the best of my knowledge, loop quantum gravity is also rather short on testable predictions). The only utility of quadruply hypothetical advances is to science fiction authors. And I've greatly enjoyed many such stories. But it's important to distinguish between science fiction and what we can do in reality.
I mean ... 800 pages, I'd say the benefit of the doubt applies.
And (my hot take:) the formal correctness is important, but not really that important in math. Sure, we hope the proofs are correct, but the idea why the proofs are correct is often more important. Humans are not a formal verification machines, and we're often interested in why something is true (and when exactly, i.e. how does it generalise), instead of just asking a binary question. So taking this into account, even if there are holes in the current argument, the important thing is that the experts believe they can be fixed, and the insight we gained along the way.
Edit: I want to back my hot take a little:
* The four color theorem is famous for being the first major theorem to be proven using a computer (using exaustive search on a large search space - too large for human to verify). This was very controversial for the time (maybe still is), because we gained no insight into the problem! Exhaustive search doesn't begin to explain why this is - or is not - the case.
* Even more perversely, It's possible that ABC conjecture was proven in 2012 by Mochizuki. But the proof is very hard to read (very briefly: basically nobody understands it, and Mochizuki was - supposedly - very non-cooperative and refused to answer questions. Some experts claimed holes but their concerns were - quite rudely - dismissed as misunderstanding). Now we live in a split world, where most of the world consider the conjecture unproven (because we can't understand it and learn from it), but some universities consider it proven (because Mochizuki is an expert, and nobody was able to find a mistake and convince the world they're right). In other words, it's a mess.
In both cases, the problem was that we care about understanding the problem, not about just asserting something is true or false.
* https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ discusses a few recent usages in recent papers and the author's grant to formalize Fermat's last theorem.
* The liquid tensor experiment (https://www.quantamagazine.org/lean-computer-program-confirm...)
* Feit-Thompson was formalized in 2012.
I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.
> The solution for these irreducible representations came to Raskin at a moment when his personal life was filled with chaos. A few weeks after he and Færgeman posted their paper online, Raskin had to rush his pregnant wife to the hospital, then return home to take his son to his first day of kindergarten. Raskin’s wife remained in the hospital until the birth of their second child six weeks later, and during this time Raskin’s life revolved around keeping life normal for his son and driving in endless loops between home, his son’s school and the hospital. “My whole life was the car and taking care of people,” he said.
> He took to calling Gaitsgory on his drives to talk math. By the end of the first of those weeks, Raskin had realized that he could reduce the problem of irreducible representations to proving three facts that were all within reach. “For me it was this amazing period,” he said. His personal life was “filled with anxiety and dread about the future. For me, math is always this very grounding and meditative thing that takes me out of that kind of anxiety.”
"If I'm designing a Research Institute, would the ideal design be something where you have babies screaming, and people are sleep-deprived, and you know, and are bombarded with responsibilities, and then they would produce better research?"
I have however the impression that some distractions of life are more fundamental than others. If the distraction is that you might not have food tomorrow or you fear for your safety, indeed I doubt you can focus on research. However other things like babies crying and "responsibilities" are only a distraction if you let them. My mental model is that "doing research" is somewhere is Maslow's pyramid which is not the bottom, but it's not as high up as most people would expect either. I'd like to hear other people's thoughts.
And "this stuff" to which you refer is the intended output of their full time jobs*. So presumably, they find time to work on it in the same way a software developer finds time to write code. You just sit down and do it, because you are being paid to do it.
*Did I miss something about how these papers were developed in their spare time?
As an aside, Europeans have families, lives, distractions etc just like people in the US. Source: have lived in Europe for 30+ years. Have a family and lots of distractions. Have not proved any major mathematical theorems. (yet I suppose- there's still time)