Something is on fire. Literally or figuratively.

Also... One of the only industries/products where unusable product/seevice (token / context burned) is neither refunded let alone even acknowledged. I wonder how many millions of dollars of inference have been stolen during these outages? First you lose the work in flight, then you lose the time, and finally you lose the token burn for a second time. What a fantastic time to not have any regulations if you're rich and greedy!

Just like a software engineer who gets sick or has to pick up their kids or has an appointment. We're used to this, oddly.

It's called compassion. We accept that humans are imperfect because we too are human and imperfect and it's the right thing to do.

We should hold corporations valued in billions to a higher standard than a single person trying to care for their family.

I'd argue that it's not even corporations anymore of which we should try to hold accountable. It's very clear who is making these calls as the players involved (Musk, Zuckerberg, Altman, Amodei, Thiel, Karp, Luckey, Langley, Nadella, Bezos, Pichai, Tann, etc) want nothing more than to be in the limelight and "preach" to the masses that they know best. They're more brazen year over year as they gain confidence in their unchecked power and continued accrual of wealth. The more money the more disconnected from reality and the stronger assumptions they build. And they have zero compassion. All of these people are dangerous to humanity individually, but when you start to realize how many have emerged and have no filter or checked powers publicly that becomes a truly terrifying thing.

I've recently started reading "End Times Fascism" [0] and it truly encompasses where we are at, how we got here and the bleak future we may be in for if we don't get in front of this now. But this book definitely highlights a lot of what some of the tech community has been seeing and hand waving about for years. The worn out trope that we should hold corporations accountable doesn't work. We should hold the people at the top accountable like other nations do because if they want the limelight then they should bear the responsibility that comes with abuses. The US is becoming a caste system by design. National surveillance, erosion of access to resources for personal compute, bought and paid for politicians and laws that don't apply to the wealthy.

[0] https://us.macmillan.com/books/9780374621384/endtimesfascism...

It's actually nothing like that, and is surely not how it's marketed or sold. I guess you're OK paying a monthly fee for Internet and having the access be unavailable for random parts of your working day because you want to anthropomorphize it? The defense with which people will go to bat for these shitty companies is wild.

Has Lean proved the Four Colour Theorem? I thought only Rocq had.

It’s an aggregated list, not a list of formalisations in Lean - the checkbox is “things formalised in any prover”.

AI is hopeless at using existing code, it likes to append only.

It doesn't seem execution was a problem. From Kevin Buzzard's blog:

I’ve compiled the code base and run comparator on it — it checks out. It is a gigantic proof (over 13.4 million lines of code) and takes nearly 20 times as long to compile as Lean’s mathematics library (on a machine with 96 cores!). Lean can be sluggish when jumping from file to file on a repo of this size (even on a machine with 500G of ram, which Anthropic also gave me access to), but Anthropic also supplied me with some html documents which are easier in practice to explore (clone the repo and open with a web browser).

500G of RAM is not actually that huge tbh (I was looking to buy a used 1TB server blade for some personal stuff a while ago but it was too much hassle) so I don't guess there was too much potential for buffer overflows.

Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it.

I’d wager a million gazillion bucks that this is not the case.

So would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?

I would say it’s very unlikely to be the case here at least.

Of course some bugs in Lean may exist (I don’t have deep insight into Lean’s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof.

As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I’d be very surprised if any buffer overflows or stack overflows exist.

Such overflows are not difficult or expensive to detect, so if any were there, it should cause a crash instead of an incorrect result.

It’s not as in handwritten C where you can forget or omit a bounds check.

I’d say it is even less likely than seeing an overflow in the Core of Java cause an incorrect result (i.e. corruption instead of a crash) - because Lean uses the De Bruijn principle of reducing to a very small Core, that is easier to keep correct (others in this thread have expanded on this I better than I can I think).

Out of pure curiosity: Do you believe otherwise or have a reason to think I am mistaken?

No I don't have any reason to believe you are mistaken other than general suspicion.

Stack overflows are also trivial to check for, if one wants to. It's just comparing two pointers, plus checking for arithmetic overflow (in case the pointers run past the maximum value of the pointer type).

I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.

Not mm0?

13 million lines of code, a lot of which is new to Mathlib. So it hasn't built on what is already there but synthesised a bunch of new stuff.

LLM generated Lean code in the past has been known to exploit bugs in the Lean kernel, it would be foolish to rule this out happening again.

US centric viewpoints. The UK is running out of space for landfills. Burning it is best for all.

And reuse better.

Ridiculous bag analogy they use - I think we all have a bunch of plastic bags as it's easy to forget to take one out - much better if I remembered a cotton one.