cottonseed
Joined 15 years ago
Karma
2,959
Submissions
591
Member since
Aug 22
email: <username first word> dot <username second word> at gmail
View on Hacker NewsRecent submissions
Comment · 2 months ago
Get a soldering practice kit. If you're doing surface mount, get a SMD one. For next level practice, checkout azonenberg's rework challenge: https://github.com/azonenberg/reworkctf. He also has some YouTube video about it.
Comment · 1 year ago
You cannot bruteforce this. Exhibiting a unknotting of K with n moves only gives you an upper bound u(K) <= n. Proving u(K) = n is an entirely different matter.
Comment · 1 year ago
Those are the same. To see that, just flip over L before performing the connect sum.
Comment · 2 years ago
Proteins are linear molecules consisting of sequences of (mostly) 20 amino acids. You can see the list of amino acids here: https://en.wikipedia.org/wiki/Amino_acid#Table_of_standard_a.... There is a standard encoding of amino acids using single letters, A for alanine, etc. Earlier versions of ESM (I haven't read the ESM3 paper yet) uses one token per amino acid, plus a few control tokens (beginning of sequence, end of sequence, class token, mask, etc.) Earlier versions of ESM were BERT-style models focused on understanding, not GPT-style generative models.
Comment · 2 years ago
I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel.
Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.
Comment · 3 years ago
2001: A Space Odyssey (1968)
Comment · 3 years ago
Yes. EleutherAI is doing it, probably one of many:
https://www.eleuther.ai/projects/gpt-neox/ https://github.com/EleutherAI/gpt-neox https://arxiv.org/abs/2204.06745
They have a 20B parameter model. I think the primary dataset for these open models is The Pile: https://arxiv.org/abs/2101.00027 (web scrape, pubmed, arxiv, github, wikipedia, etc. There is a nice diagram on page 2 that summarizes the contents.)
Comment · 4 years ago
AllSpice might be what you're looking for?
> AllSpice: A git platform for hardware engineers
Comment · 4 years ago
Where are you losing people in your hiring process? Are you getting no initial applications? Do you give the coding exercise but they never do it? Do you give an offer but they turn it down? There is a lot of speculation in this thread but you should have the data.