Ohentis

Most of this feels fairly orthogonal to the question asked. And the reasons lean are chosen are fairly simple: it is designed to also be used for programming and it's actually successful. Compiling to C is fairly obviously a bad choice (well I guess not obviously, people keep implementing languages this way for some reason) but arguably one of the least important factors in choosing which prover to use. The alternatives to lean would be Idris (which is both unsound and unpopular), ats (which is unpopular) or rocq (which is more reasonable but still is mostly an academic project).

Being more strict with how you perform operations and then using a set seed. It isn't super useful in most cases.

No, they really were (hilariously) dumb and simple. Now let me list two examples that are just vocabulary.

The motion controls make it age really poorly imo (motion controls aren't bad, but forced motion controls to do anything is)

You can just do that anyways.

I don't really think this is the case. The rules feel very consistently applied. Training is fine. Output may still be copyright infringing in some cases (but difficult to prove and none of these tech companies have tried yet). Publishing decomps is not fine and never has been. Piracy is not fine and never has been (and anthropic got in trouble for it). The only case that I know of where an AI company got off free for something an individual would be punished for is the various hacks that they've "accidentally" done.

From this comment it isn't clear if you previously thought it stood for polynomial and non-polynomial and have been corrected or if you still have this misconception, but just in case: it actually stands for polynomial and nondeterministic polynomial. P is a subset of NP, they aren't opposites. And yes most people intuit that they likely aren't equal.

It just seems like we're missing some pretty important stuff. The amount of "training data" humans process in out lifetimes is nowhere near enough to achieve the abilities we have, so clearly the bulk of our brains abilities must be hereditary. The only problem is: by what mechanism? Is such a complex model able to fit on a single cell? Are we somehow influenced by our mother's body in ways that are outside of that thinking? Are our brains just somehow much better architecturely than current ml approaches? The more I think about the more I feel that true AGI is probably still lifetimes of knowledge away.

It isn't actually Jevon's Paradox, but nearly all products behave that way (law of demand). There are exceptions of course, but it would be surprising for it not to apply here imo.

In some circumstances you might not need to anti alias if you are using pixel art. In some circumstances you do. Either way it largely won't hurt.

I somewhat doubt it. Having many people, even at your own company, know your private key seems like a problem of it's own. In fact it's likely to me that no human has ever seen it until now.

I quite like how i2p does it. Public keys are part of addresses, human readable names are user defined and shared but static.

I guess you could do some SNARK like proof. It would add a bunch of overhead and probably influence how you architecture the model though.