j2kun

I'm going to start using that term :)

Tort law does not. This seems like a case of dangerous instrumentality.

Unfortunately, marketing, hype, and venture capital overshadows any serious public discussion of capabilities.

That may be true, but I hate it when people repeat the false idea that functional equivalence requires only a test suite that has full branch/line coverage. Call me triggered :)

That said, I would probably follow this same approach if I were to do this, but with extensive randomized testing as well.

I struggle to believe that someone would find it worth that much money to have a decompiled version of a game they also commit to keeping private.

Functional equivalence here, of course, depends on the completeness of the test suite, where byte-identical compiled artifacts does not.

(For example, your approach would not necessarily catch all the same overflow behaviors; the OP expressly claimed that "replicating all bugs" was also important, and many bugs are caused by certain overflow behaviors)

I imagine this would go far, but also note that the variety of compilers used over the last 30 years of game dev would make this not so obviously generalizable.

> specific choices of notation are identical to a preliminary version of the present paper

I don't see how it's related to quality at that point. Call your technique "the banana method" and wait to see OpenAI invent "the banana method"

And if the same AI has tried and failed to break lattice problem security, wouldn't that suggest the problems are more secure, not less?

I stand corrected!

FWIW, there has already been a lot of effort thrown at AI attacking lattice problems underlying PQC without anything to show for it. I'm not sure why Vitalik is suddenly worried about lattice problems in particular, unless he has some insider knowledge.

I think this depends a lot on what you plan to do after your PhD. Moving to industry you will likely not use the direct work of your PhD, and instead you will rely on your broad knowledge, intuition, rigor, ability to learn hard things, and extend that to bring new research developments into practice, all of which are largely unrelated to AI scooping math proofs of prize problems.

AI is producing works that are so poorly written/explained that it requires AI to even parse the results, which in turn produces explanations that are still confusing. In fact, it seems the humans are required to understand and explain the results, and the fact that they need to use AI to do so is a shortcoming of AI.

And if humans decide to give up on mathematics because the process of using the machine is so tedious, then there will be no value in automated theorem proving.

People described the problems as solved the minute they were made public.

I used to think this and then I saw how well webp reduced my website's bandwidth costs compared to optimized jpg or png. I felt a bit left behind at that moment, like I should have been paying attention to these great improvements over the years.

I would say it's released in the spirit of machine learning's competitive landscape (which is the culture this emerged from).

Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.

Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."

I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them.

The idea that an AI company is beyond peer review is harmful.

> All the major AI-generated proofs so far were done by AI without using lean

Is that true? I was under the impression they used lean as they went.

> rather than to Lean

Indeed, I don't think anyone should be led to believe that AI can do math on its own without _some_ kind of oracle providing extremely rigorous feedback.

> In modern times, everyone knows that writing assembly is a fool's errand

ffmpeg is like 10% assembly. I think something similar is true of all video encoders. OpenSSL and libsodium write some of their core math routines in assembly (e.g,. NTT).

So maybe this myth should die?

Sounds like they should charge for software updates then, as that is directly related to the ongoing work for people who have already bought the software.

You don't need AI regulation when you have the power of the purse.

that sounds ridiculous. How could it be so much cheaper

Why in the world would that specific 3x3 matrix be a trigger for an attack? Are they trying to find someone doing some particular kind of numerical analysis?

It's a good point, and it also depends on the feature being good and sensible and in demand enough to push users away from the default.

And then it incentivizes people to make good forks, like neovim vis-a-vis vim.

Zero-knowledge seems completely unnecessary. Surely the original image does not have any material content in it that is not made public by publishing a JPEG-compressed version.

Could this be simpler and more efficient without ZK?

Perhaps one thing you should devote effort to is ensuring this has not already been proved in the literature.

> Did the theoretical math lead to the invention of GPS, cryptography, lasers, etc?

For cryptography, perhaps you would enjoy reading the paper of Diffie and Hellman that proposed public-key crypto: https://ee.stanford.edu/~hellman/publications/24.pdf

You will find they were inspired by the NP-hard knapsack problem, and inspired a bunch of later research that led to RSA.

I think the tapestry of history would suggest the answer to the question "is math responsible for this invention" a lot more complicated than it appears. For lasers, Einstein proposed the idea based on purely theoretical physics, and it was made possible in 1960. Is that "theoretical math leading to the invention of lasers"? Surely he was at least relying on a lot of additional theoretical work for that. On the other hand, much theoretical that came out of Bell Labs were responses to needs for better vacuum tube technology, better amplifiers, etc., which were a deep collaboration between theory, practice, and tradesman with a strong intuition for how to build with various materials and at varying scales.