rencrisa

It may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.

Even beyond cheating with sorries or kernel bugs, the lean encoded theorems (or specifications) must be checked by humans to see if they truly mirror the real theorem authentically.

It seems that a lot of folks misunderstand the guarantees that lean provides.

I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications), that the lean proofs are checked against, indeed correctly encode the real theorems. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.

I just want to state that having "lean proofs" that build does not mean the actual real theorems we care about hold. Ultimately a human has to verify the lean encoded theorem statements that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal.

It seems that a lot of folks misunderstand the guarantees that lean provides.

I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications) that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.

> nowadays all PhD students generally take something called “Responsible Conduct of Research”

I think that is a broad generalization. I never had to take an ethics in research course as a PhD student.

> falsifying data, plagiarism, how to ethically work in animal models ... image manipulation.

My take is that this may be a "field"-dependent class. My PhD is in a non-experimental field (math); thus, we cannot have these sorts of issues (minus plagiarism).

A video documenting a food youtuber's experience of getting ransomware, and trying to recover access to their accounts.

TLDW: Know someone at Google, and they can fill out an internal form.

AES256 is still secure, assuming the encryption key has ~256 bits of entropy (32 random bytes). Assuming your master password is reasonably complex, hopefully the encryption key derived from your password has enough entropy.

Despite this, I recommend rotating all passwords (if you don't have the time, prioritize rotating passwords on important accounts / putting MFA on them). For all we know, lastpass might have had a full compromise (i.e. access to unencrypted vaults from malicious source code commits).