But Manus's IP was already transferred and in any case Meta is not legally doing business in China, so Manus will still live on, possibly get rebranded.

To illustrate, let's say you want to verify a "Hello world" program. You'd think a verification involves checking that it outputs "Hello, world!".

However, if a contractor or AI hands you a binary, what do you need to verify? You will need to verify that it does exactly print "Hello, world!", no more, no less. It should write to stdout not stderr. It shouldn't somehow hold a lock on a system resource that it can't clean up. It cannot secretly install a root-kit. It cannot try to read your credentials and send it somewhere. So you will need to specify the proof to a sufficient level of detail to capture those potential deviations.

Broadly, with both bugs, you need to ask a question: does this bug actually invalidate my belief that the program is "good"? And here you are pulling up a fact that the bug isn't found in the Lean kernel, which makes an assumption that there's no side-effect that bleeds over the abstraction boundary between the runtime and the kernel that affects the correctness of the proof; that safety guarantee is probably true 99.99% of the time - but if the bug causes a memory corruption, you'd be much less confident in that guarantee.

If you're really serious about verifying an unknown program, you will really think hard "what is missing from my spec"? And the answer will depend on things that are fuzzier than the Lean proof.

Now, pragmatically, there many ways a proof of correctness adds a lot of value. If you have the source code of a program, and you control the compiler, you can check the source code doesn't have weird imports ("why do I need kernel networking headers in this dumb calculator program?"), so the scope of the proof will be smaller, and you can write a small specification to prove it and the proof will be pretty convincing.

All in all, this is a toy problem that tells you : you can't verify what you don't know you should verify, and what you need to verify depends on the prior distribution of what the program is that you need to verify, so that conditional on the proof you have, the probability of correctness is sufficiently close to 1. There's a lesson to learn here, even if we deem Lean is still a good thing to use.

Let's have a thought experiment.

If we take the prevalence of false accusations be several thousands a year (the lower end of the estimate), it would be between 1 to 2 incidents per 100k population in the US. For your UK statistics, I can't find a citation either - in terms of prosecuted cases you're perhaps right, again the buck doesn't just start with prosecution. Reported rape incidents can be up to 70k and prosecuted incidents is less than a tenth of that, and it's probably similar for false accusations - what I can find is an estimated prevalence of 3%, so in the UK it would be up to 2.1k among reported (not necessarily prosecuted) cases.

Incidentally, 1 to 2 per 100k is in the ballpark of rape statistics in low-crime areas, such as Hong Kong, Japan or Singapore. So the risk of rape in those areas is similar to the risk of false accusations in the US.

With this in mind, if a woman denies a ride to a strange man in Hong Kong in the middle of the night, does that mean she was nasty to the man? If you say yes, it's probably not the prevailing sentiment in those areas; if you say no, perhaps that can point to some cognitive bias.

For unions, sure let me know when you're able to set them up. Similarly, you can tell women in Hong Kong or Singapore to not worry about rape because you're going to do something to make the world better for them. But another important nuance is that unions won't help as much as you think they would. In the case of false accusations of pretty much anything, a lot of the damage is social, for people who are not already powerful; rape is an especially touchy topic that you would find fellow union members, especially female members, and sometimes spouses, to be less than sympathetic.

For them to survive, they have to have got returns from somewhere - maybe welfare, inheritance, a day job. Someone has to have worried about the returns so they can be free from thinking about it.

And if you don't worry about returns, you will let someone extract it ruthlessly from you, that you contribute millions of value to a company that gives you nothing back. This may be fine to you at some level, but many of the people who you allow to exploit you use the resources they gain as leverage to further their selfish ends, like a certain richest man in the world who helped a certain politician buy an election at the most powerful country in the world.