(not a mathematician, but I played with lean as a hobby). No, this already existed - lean standard library was basically this, with hundreds of mathematicians working together to formalize basics of currently known math. But this is just very slow for a human.
I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible.
In short, no, lean was not a tool to discover new math.
>Healthcare makes up the lion's share of that spending;
I heard US healthcare, rather famously, spends more per capita than any country in the world, despite still being rather terrible. Maybe the solution is actually reforming it in an European way (including universal free healthcare)? Your other points are very interesting to me, especially negative feedback loops of austerity - I never thought about that before.
The primary factor (in my view) is that we pay healthcare providers (doctors and nurses) 2x to 3x as much as other developed countries.
That creates knock-on effects throughout the healthcare system:
* Doctor time is worth $xxx/hour, so every second counts. We hire a bunch of support staff to make sure doctors aren't "wasting" time on paperwork, taking vitals or talking to patients. Now it costs more to run a practice.
* Doctor time is worth $xxx/hour, so we need to make sure that health insurance only pays for procedures that people truly need. That leads to insurance companies hiring a bunch of doctors and nurses to adjudicate claims (that's expensive, plus fewer doctors practice medicine). It also leads to denied care.
* Doctors have a lot of money, so if a procedure goes bad and you want to sue someone, they make a juicy target. Now you have higher malpractice insurance, so doctors bill even more.
* Doctors are afraid of being sued (see previous), so they often order more tests than necessary to prove they are providing adequate care. Those tests cost money.
The cause of high doctor salaries is an artificial shortage of doctors. Medical schools collude to limit the number of medical students who matriculate each year, which squeezes supply.
We could very easily fix the American healthcare system in about 10 years by simply allowing doctors and nurses trained in other developed countries to practice here, plus forcing medical schools to accept more students.
Regarding the latter, there is no shortage of qualified applicants:
1. Nearly everyone who starts medical school finishes. Matriculants are so statistically overqualified that hardly anyone washes out.
2. Medical schools have silly-stupid entrance requirements which have little to do with being a good doctor. Beyond GPA, you need many hours of volunteer work outside of class, extracurricular activities, and often research experience. These admissions requirements are imposed because there are simply too many qualified applicants for the number of slots and med schools need some "fair" way to cull the herd.
Yes the US could save a ton with a more efficient healthcare system. Additionally we have shockingly high costs for basic infrastructure as compared to other developed nations which could also provide savings if we could streamline that.
For the economic impact of austerity there has been a lot of good scholarship about this recently. Check out Austerity in Crisis?: A Narrative Review of Its Economic, Social, and Political Effects in Times of Crisis https://arxiv.org/abs/2510.10449
It isn’t as hopeless as it looks. Places like Oregon have been long experimenting with things like coordinated care organizations to better manage healthcare. Also health system like Kaiser Permanente compare more favorably to national healthcare systems than you might think.
>It's almost like there was a Republican-policy-created crisis that called for massive spending in his term.
As an European it's pretty funny to read this thread. "Your party debt was reckless and incompetent. My party debt was necessary and caused by your party anyway". Seriously, having just two parties looks like nightmare for democracy.
Having said that, before I get crucified as a centrist, there are bad and worse, and Trump is clearly worse.
The level of debt is an issue when the revenue doesn't cover the spending, leading to a budget deficit. Obama reduced the deficit even after he increased the debt. Trump increased the debt and reduced the revenue widening the deficit. That's not the same thing.
I don't know why, but 2^32 search space is WAY too small. Anything they could enumerate back then (or even today) is way too small. This is like saying they tried four times before they found a vulnerable one.
I can't tell if this is sarcasm, or do you honestly consider credit for fast food a good thing. I hesitate because I know that in America people buy everything with credit (or at least a lot), so it's possible some people think like that. But obviously not buying fast food with credit is a good thing?
You're not helping your case by being arrogant. FWIW the person you're discussing with sounds a bit more balanced in their opinions. I am open to changing my mind, but refusing to elaborate because it's a "waste of your time" means conceding your case.
What precisely is arrogant about refusing to give somebody a history lesson about the labor movement when all of the information necessary is available and trivial easy to get?
I have no case to make here other than the one I’ve made: the representation of the labor movement that was made is completely incorrect
Because it runs counter to your stated goal of convincing those reading the conversation to not take your interlocutor seriously. I really think if you're tempted to write a "I'm not going to argue with you" comment you should just not post at all: it damages your position less.
(This is a particular technique that seems to have been picked up because of gish gallops/sealioning where the goal is to just fill up the space and wear down any objections, but I think this cure is worse than the disease: explicitly refusing to engage, even if apparently justified by the expert view of the arguments you are rejecting, really only makes you look weaker, more unreasonable, and more out of touch to onlookers on the fence than walking away. I think it's a real hazard because it's emotionally satisfying to you and people who already agree with you while utterly corrosive to your credibility to anyone else)
Not a counterpoint, actually case in point, because:
>Mochizuki and a few other mathematicians claim that the theory indeed yields such a proof but this has so far not been accepted by the mathematical community.
Well nobody needs to use IDE. There were always people who used vim with tmux as their IDE. The value of IDE is the I as in integrated - I see some value in having easy to manage single dev environment with batteries included. (I'm not an IDE guy though, and I personally closer to vim/vscode + plugins)
There were always people who used vim with tmux as their IDE.
But until language servers, IDEs with built-in code analysis had a huge advantage. This stopped once LSP was designed and some language servers got mature. LSP was developed originally by VS Code and it is easy to see why - it allowed VS Code to compete with IDEs without writing their own code analysis by letting language developers write a standard server. This made VS Code (and others like Zed) so powerful, that they had already replaced IDEs for many users (maybe outside Java). LLMs are just another nail in the coffin.
No, it didn't stop. In my experience, LSPs are still incredibly poor and comparatively primitive vs the actual analysis that JetBrains have implemented. It's night-and-day different in terms of the supported refactorings, actual understanding of the types and the codebase etc.
Also, LSP is just poorly designed and inefficient. JSON-RPC was an awful choice, the specification text is not well-written and the whole thing feels like a Microsoft pet project for VS Code than an open specification that everyone agrees works well.
I think the name misleads people about LSPs. LSPs are basically plugins for VS Code. The protocol semantics are visual, so they're tied to what VS Code wanted to display on screen. They don't really change the game, especially as you always had the option of using IDEA's own plugins in other tools and text editors (yes! there is an API and you can start up a headless IDEA to access it, even from programs written in C or Rust).
Not many did that because JetBrains never cared much to properly document this path, and so using LSPs is a better paved cowpath. But that's because IDEs aren't a real business for Microsoft, whereas they are for JetBrains, and we know where that leads - the landscape is filled with the skeletons of dead IDEs that were just loss making corporate side projects, defunded and "donated" to some foundation once the executive sponsors moved on. NetBeans and Eclipse are two of the most obvious but there have been others.
The risk with VS Code is it goes the same way. Eventually Microsoft needs to cut back, perhaps due to needing more capital for AI or due to AI related losses, and in the general layoffs that follow VS Code gets cut back to a skeleton crew.
This is not the whole picture. IDE is not just for writing code. What I really like on jetbrains is how strong the platform is. I will show you example which would be great if they implement it.
If you use ideavim you can enable feature which shows you action ID you have currently triggered (Ideavim: Track action IDs). If you click on anything it will show you name of that action and you can setup vim shortcut for that. This way, you can use almost anything by just typing a few letters. But that is just a start.
Now imagine you can use this to create "macro" which will create something like skill for LLM. So in a few seconds to minutes you can create "skills"/runbooks for major refactorings, project updates, git bisections, project deployments, log analysis or whatever you can think of. You will just click on 20 features and it will record what you did with some additional context (files, connected services, build systems etc.). This is the strength of integrated tools.
Of course this is just my imagination but I am not the smartest person in the world and I am pretty sure/hope that someone in jetbrains or in other IDE company is thinking this way.
You envision a world in which humans don't look at code.
I think that world is farther off than you think, especially in critical line of business software. You can YOLO it with your internal dashboard or your hipster coffee review site, but in my 2M-line highly regulated banking system, humans sign off on the code - even if LLMs do most of the typing.
>it's a choice to refuse to reuse what was trusted yesterday in order to build the next stage.
If the point is to let independent people verify the full build chain, then there is no "trust from yesterday" to reuse.
Even worse, if every release N depends on trusting release N-1, then you need to do a full rebuild of everything in the whole history, instead of just building the current release. This doesn't sound reasonable, or at least sounds incompatible with the project goals.
I want to read content only in a specific language. This is different language than the language of the country I live in. I have my operating system, my keyboard layout, my browser, my accept languages header, everything configured to the language I want.
And get I often get websites and ads in the language of the country my IP points to
I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible.
In short, no, lean was not a tool to discover new math.
reply