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).

@utopcell do you have a reference for incremental FFT? I'm not sure if I understand what your implying.

Given a polynomial f(X), obtaining f's evaluations over the n-th roots of unity takes O(nlogn) using FFT. Are you stating that obtaining g(X) != f(X) evaluations over the n-th roots of unity should take O(n) time assuming some precomputation derived in the FFT for f?

I am in a CS PhD at a top 10 institution, and I've had a great time in my lab. My advisor has a saying "You can never make me do something I'm not interested in!" Thus, I've personally never worked on anything I didn't enjoy. I learned a lot from my lab mates and my advisor.

Of course, I think this is super dependent on the subfield and advisor. Based on our department surveys, ML / AI / Graphics students rated the lowest in satisfaction, happiness, and highest in hours worked per week. While, Theory, HCI, and Systems are overall pretty happy and have regular working hours.

EDIT: In response to other threads, my pay is also very comfortable. I can take vacations, eat out, and afford a nice studio apartment. Free health insurance as well.