Oops, yeah, my bad. I&#x27;ve been doing a deep dive into lean4 and ended up conflating the use of the term computability from that context. Sorry, for the confusion!

Can you say more about computability of &quot;conformal models&quot; in the Langlands context (beyond vibes, perhaps cites)? In my understanding, &quot;conformal models&quot; are by construction computable..

This is exciting news! Though, there is more than just the math that needs to be done here. Namely, mathematicians not only need to formalize a concise language to bridge the gap with modern conformal field theory, but they will also need a way to understand the computability of models based on this system. And yet, there is also the human factor: namely, there needs to be an effort to sell this paradigm to existing theorists, which will require substantial effort.

Prior:<a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=40280760">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=40280760</a><a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=40453822">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=40453822</a>

I&#x27;m not sure that&#x27;s true. My quick searching around is that the first paper proposing strings as a possible description of space and time is Nambu, Nielssen and Susskind in 1969 whereas Langlands first stated his conjectures in his letter to Andre Weil in 1967[1] (ie before string theory had even really kicked off mathematically which didn&#x27;t happen until Ed Witten got involved in the 1980s). In his letter, Langlands seems to motivate the conjectures entirely from abstract algebra and topology (although this is way above my mathematical pay grade at the moment so I&#x27;d be more than happy to accept I misunderstand).[1] <a href="https:&#x2F;&#x2F;publications.ias.edu&#x2F;rpl&#x2F;section&#x2F;21" rel="nofollow">https:&#x2F;&#x2F;publications.ias.edu&#x2F;rpl&#x2F;section&#x2F;21</a> and <a href="https:&#x2F;&#x2F;publications.ias.edu&#x2F;sites&#x2F;default&#x2F;files&#x2F;letter-to-weil-1967-01_rpl_1.pdf" rel="nofollow">https:&#x2F;&#x2F;publications.ias.edu&#x2F;sites&#x2F;default&#x2F;files&#x2F;letter-to-w...</a> in particular

Not particularly, it&#x27;s so open ended it describes an enormous landscape of possible universes and lacks any specific testable predictions for our universe.Unless it&#x27;s been firmed up a great deal in recent times.

String theory is still the only self consistent theory of quantum physics.... I&#x27;d say that&#x27;s extremely successful.

I&#x27;m curious what applications there might be if any in number theory. If I recall, langlands had motivations from string theory concepts which ultimately wasn&#x27;t as successful as hoped in physics.

Article and interspersed visuals were a pleasant learning experience. I&#x27;m not caught up on mathematics as much as I&#x27;d like to be..

What exactly do you mean by non-trivial&#x2F;modern standards? While certainly the largest and most complicated theorems are currently out of reach of proof verifiers, there isn&#x27;t a shortage of usage of them to prove important&#x2F;modern theorems (of course certain fields are much more developed&#x2F;more amenable to verification than others).* <a href="https:&#x2F;&#x2F;xenaproject.wordpress.com&#x2F;2024&#x2F;01&#x2F;20&#x2F;lean-in-2024&#x2F;" rel="nofollow">https:&#x2F;&#x2F;xenaproject.wordpress.com&#x2F;2024&#x2F;01&#x2F;20&#x2F;lean-in-2024&#x2F;</a> discusses a few recent usages in recent papers and the author&#x27;s grant to formalize Fermat&#x27;s last theorem.* The liquid tensor experiment (<a href="https:&#x2F;&#x2F;www.quantamagazine.org&#x2F;lean-computer-program-confirms-peter-scholze-proof-20210728&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.quantamagazine.org&#x2F;lean-computer-program-confirm...</a>)* 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&#x27;t mean formal verification of a proof is completely orthogonal to understanding it - you can&#x27;t formally verify something without really understanding the proof in the first place.

No nontrivial (by modern standards) proof has a machine-verifiable version. Math is just too huge.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&#x27;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&#x27;t begin to explain why this is - or is not - the case.* Even more perversely, It&#x27;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&#x27;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&#x27;re right). In other words, it&#x27;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.

Is there a machine-verifiable version ?I mean ... 800 pages, I&#x27;d say the benefit of the doubt applies.

Quote from Knuth:&quot;If I&#x27;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?&quot;<a href="https:&#x2F;&#x2F;github.com&#x2F;kragen&#x2F;knuth-interview-2006">https:&#x2F;&#x2F;github.com&#x2F;kragen&#x2F;knuth-interview-2006</a>

The article does in fact discuss precisely this:&gt; 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.&gt; 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.”

By my count at least four of the researchers are employed by American universities and therefore most likely live somewhere in the United States.And &quot;this stuff&quot; 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?

Interesting, Alexander Friedmann, another notable solver of Einstein equations, also fought in WWI, though on Russian side :)

Similar for the Choleski decomposition. Also artillery officer in WWI. Died in battle.

Jean LeRay invented sheaf theory while he was a POW in Austria in WWII.

Karl Schwarzschild found the first exact solutions to Einstein’s gravitational field equations (general theory of relativity) while serving in the trenches in WWI, firing artillery at the Russians.

In the article one of the authors of the proof describes a key breakthrough as happening when he contracted covid and was thereby forced to spend 3 months in bed with nothing to do but think.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&#x27;s still time)

Mathematical research (as far as I know) requires significant amounts of ‘time off’ just pondering and meditating on ideas as much as it requires time sitting at a desk concentrating on a paper or working through things on paper. A lot of people have said their best work was done whilst standing waiting for a bus, in the shower, walking in the woods …and so on.

How do people even find the time to work on this stuff without being distracted by life, family, and everything else? I think this is why so many of these people are in Europe. America is too chaotic and full of obligations and distractions to do serious academic work.

Monumental proof settles geometric Langlands conjecture