jojomodding

Math is not about the definitions. It is about the connections between these definitions. And the techniques used to establish broader classes of connections between similar objects.

The way we formalize a connection is with a proof. And if the proof is "nice and modular" it sorta explains by itself how it can be used for similar problems.

And such proofs definitely belong into MathLib. There is often value in actually reading the Lean proof script (especially with the IDE support like jump to definition). It is not only there for the machine.

"Reading" a textbook is very different from reading a novel, that should be noted. You gotta do the exercises.

And who is "they" in this case?

Or alternatively, instead of evicting it all, can you move the data around in physical memory while updating the page table, so that you can clear a large enough continuous block of physical memory?

Not so fun fact: Mythicism around Proto-Indo-European is part of what made Hitler come up with the idea of "Aryans" because they hypothesized that there was some relation between the language having come from Iran (as "Urheimat") and then this leads to everyone wanting to be (indo)-aryan-decendent the most.

Yes it is true in the unique model of second order PA, aka the computable model, aka the "standard" model.

They still have scientific instruments operating. These have produced new insight into the last few years, telling us e.g. how large the Heliosphere is. The investment needed to find this out with a new drone would be astronomical (heh) whereas using the existing tools is basically free.

Yes, in particular the slides by Kevin Buzzard (linked in there or here: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... ) are funny and educational on that matter.

No, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample.

Football was doing fine before this all started. It just multiplied the wages of some people who already earn more per year than I will ever own in a lifetime.

Yes. One way to do so is by eradicating gambling (or at least the ads for it).

People will never be 100% happy, all the time. And gambling (like many other companies) prey on people in the moments where they feel down.

Chaitin's constant. Or rather, you can never see that it has been laid out in your infinite universe.

They just need to have smaller fees than Visa/Mastercard.

Paying by SEPA direct debit in a store checkout situation seems insane. Even with instant payments it can take 20 seconds which is too long. Add to that the fact that users need to log into their online banking and the unfair leveling of risk onto the consumer.

This video is so insane. They're in a combustion engine. I can not fathom why they survived let alone managed to drive out of this. Trains are not build for fire resistance.

Is it gonna be one of those things where increased safety encourages dumb people because "it is watertight you know" so now a lot more people drive into the floods, and even though it's a smaller proportion more people in total drown.

I am not sure I understand what you are trying to say. There is currently a lot of demand for building out solar and wind in Germany. There is also large demand for building battery storage. The demand especially for the latter comes from the mismatch between supply and demand in electricity markets, so in a sense the battery operators hope to do arbitrage in a way that will also increase the efficiency of the market (by allowing the use of solar after dark).

This is very much a market-based solution. What the state has to do is provide permits and stuff for getting the batteries etc. actually built; which the state is doing but not as fast as it could right now. (at least in Germany)

You can never know. People in Germany have wildly divergent takes on what would be good for the country right now and some things that are acceptable to say in mainstream circles seem batshit insane to me.

The non-profit (the Foundation) pays for specific things but it is not really there to hire people to work on things. It pays for infrastructure work and to pay the existing maintainers who often do review work. It also gives stipends to up-and-coming contributors for Open Source outreach programmes, but this are not really the people who you want to have immediately work on your critical infrastructure code.

Probably criminally liable for bankruptcy as well. At least in Germany (where I am vaguely familiar with the law) you lose bankruptcy protection for debts you take on that are knowingly not covered by existing assets or expected future income. This is usually hard to prove, but if your assets are 0 and there was never a viable plan all along they'll likely found you guilty. This means you become personally liable to the creditors and might also face jail time.

You can tell this is a true success in Germany because 95% of local passengers now use it. It also caused a significant increase in ridership, putting the already overloaded rail system under a lot more pressure while taking away income from the rail companies (after making it cheaper).

Ah, that's what they're building the power plants for. Blasting things into space.

In times like this, I am happy I live in the EU where I can request a company send me a copy of all data they have stored about me. That includes all pictures I ever send to them, or at least a low-resolution preview sufficient for me to realize which picture it is, or at the very least a file listing. Ah yes and they must do so without charging me anything.

The judge will decide if the evidence is admissible or not.

Switzerland already has such a party, the SVP (UDC in French), and in fact they put forward the initiative.

This was widely understood to be a vote on how well the SVP can appeal to the center. Turns out pretty well but it's not entirely surprising given their recent election results.

Newspapers have mechanisms like corrections and apologies that can be used to "right" a published falsehoods.

This relies on me being able to find out if a newspaper lies about me, which is usually easy since we can all go buy the same newspaper. With AI it is much harder to find out that it has been telling potential customers wrong things about my business.

Well, you can use tap code: https://en.wikipedia.org/wiki/Tap_code

Or you can use "Morse tap code" where two close knocks represent a dot, and if the gap between them is slightly longer it's a dash. That takes two knocks for one dot/dash but it works and is (was?) used in practice.

Most countries you would consider "developed" in the world (and then some more) switched to having a professional, non-political civil service in the last 100 years, if they hadn't already had one.

Do you think that this maybe indicates something? Or did your analysis stop at the US border? Is it wise to base policies on a system that has not been used in more than 100 years based on the perception that this was some sort of golden age even if a cursory glance around the world show that no country you want to live in is run like that?

Once it shortens the loop, the compiler can also observe that `tab` is a local variable and therefore move the writes up "to the initializer." It can then see that the variable is unused and delete it, and also delete the loop.

Interestingly, the way in which Grothendieck conceived of equality is nowadays being questioned, especially due to the rise of formalized mathematics and Lean. More concretely, there is this fun paper by Kevin Buzzard which deconstructs it: https://arxiv.org/abs/2405.10387

Money quote:

> In this paper I argue that the first assertion above is false, the second is dan- gerous, and the third is meaningless.

This also makes it obvious that at some point, the halting problem becomes "unprovably hard." There must be Turing Machines for which it is independent of the accepted axioms of mathematics whether or not they halt. And indeed, constructing such machines is not too difficult.

There is current research into finding the smallest such Turing Machine. Here is one with 748 states: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...