mswphd

the apple lawsiut about hw theft at openai is ongoing lol

see the Grothendiek prime

https://en.wikipedia.org/wiki/57_(number)

those numbers are "adjusted" though. so they are not profitable by the standard definition.

helicoptors are a much more dangerous way to travel though? this is already true in the best of times/when you aren't anticipating a possible attack on the passengers.

there's a funny paper on this theme, titles "Could a Neuroscientist Understand a Microprocessor"

https://pmc.ncbi.nlm.nih.gov/articles/PMC5230747/

roughly, it reviews common techniques in neuroscience, and comes to the conclusion that they would not be able to understand even simple computing platforms that we have perfect information for (and can perfectly stimulate any internal connection, can perfectly read out the values on any internal connection, etc).

tanks have very much run over people to kill them. a wheel can very much be used as a weapon.

isn't blitzscaling essentially the same thing, except for when American companies do it (not always within their own country, e.g. spotify, netflix, or amazon)

the way LLMs write math is not beautiful. it is exactly analogous to the software that LLMs develop is not beautiful. it may achieve impressive end products, but if you like understanding the methods/architecture, looking under the hood is often a field of horrors.

I won't take a side in things, but OpenAI stated the model they used here started training August 28th. Note that "training" here might mean "post-training with RLHF an Astra base model" or something. but training had only started a little over a week earlier.

worth mentioning there's some indication the 240k peak was massively inflated by bot accounts. but by all means there are many fewer bot accounts this year, and it's still ~150k concurrents frequently. so it's still doing very well, but the numbers are a little different.

I guess I don't understand the issue you're raising. If you want to formalize a non-constructive proof, it remains non-constructive, even if you have a computer check the proof vs a human.

As a trivial example, in lean you can work with probability theory/measure theory. This has oodles of non-constructive parts, but we can ignore that for now. As part of this, you can use the probabilistic method. For example, if you want to prove that codes with optimal parameters exist, for many noise models it is known that sampling a code randomly from an appropriate (and often naive) distribution will yield a code with optimal parameters.

You should be able to prove this in lean (or any other theorem prover). But you cannot construct these codes. While you can sample a code randomly, verifying a code has good parameters is typically NP-hard (e.g. it is an instance of the minimum distance problem). So, you cannot (efficiently) "construct" a good code in lean4, despite being able to prove one exists.

This seems analogous to me that you could validate that a non-constructive proof is correct in lean4. Sure, it would be nice if the proof was constructive. But it isn't, and encoding it into a computer shouldn't give you that (non-trivial) property for free.

if Stadlmann used a previous OpenAI product, and Astra was trained off of her chat, and had a comparable approach, then it might be comparable.

they're using a new model trained since the prompts happened. They are not denying the other group's solution may have been in their model weights, despite it being unreleased.

it's very possible they only had to use the massive compute budget because they were trying to plagiarize his work before he published it though, e.g. autonomously do things in ~7 days what he had likely been thinking about for ~1 year.

you can add law of the excluded middle as an axiom. See midway down this page

https://xenaproject.wordpress.com/2017/10/05/more-easy-lean-...

this isn't really true anymore. First, a number of the big results are constructions, not counterexamples. For example the existence of a non-sofic group. It was widely believed that non-sofic groups existed (so it wasn't a "counterexample" to a widely believed conjecture), but no constructions were known.

There are other examples though. For example, NP hardness of n^{1/400}-approx CVP. Like any NP hardness proof, this shows you can faithfully encode a hard problem (3SAT here iirc) in terms of another candidate hard problem. Not really a counterexample at all.

openAI's claimed solution uses a model trained in the last 2 weeks. The prior work would definitely be included in the training set.

both wrong.

1. he was working on the same class of problems. He explicitly mentions they were working to extend their techniques to NS (the same techniques that OpenAI may have scooped somehow), and

2. while he was using LLMs to do it, this was part of fleshing out another mathematician's work in the area. He explicitly writes in his note that this other mathematician (Luis Martinez-Zoroa) deserves a Fields medal for this work.

eh, lattice-based stuff is the first time public-key crypto can use word-size arithmetic, vs full bigint (RSA), or "just" 256+bit arithmetic. it's significantly easier to get right in a side-channel resistant way.

this isn't to say everything will go perfect, but the people doing implementations are more experienced now, and the problem is an easier one to do (though in a certain sense, optimizing compilers are making any side-channel resistance a harder goal to achieve. an implementation that is resistant under one compiler version may not be resistant in the future).

and the more recent (post-quantum) lattice-based stuff can get away with ~16 bit arithmetic (it's vectors of ~512-1024 dimension, but the operations are SIMD-friendly)

any cryptography can break at any time. Sometimes "sudden" breaks happen. You can't defend against these, so there (perversely) isn't that much of a point worrying about them, besides using schemes many people have thought about for a while.

Another way cryptography breaks is via iterative improvements. For example, in the last few months there are two big cryptanalytic stories

1. The novel scheme (though not standardized) HAWK had its security reduced by ~1/2 by AI. It is no longer compelling in any way. This was in a sense "predictable" though. There was a series of papers showing that HAWK-like schemes were vulnerable to an attack of this type. Then, AI was able to bridge the gap and apply these attacks directly to HAWK.

2. The ISO-standardized scheme McCliece (from ~45 years ago) has had some alarming security reductions, and may be effectively broken (it's still a little early to tell, many cryptanalytic papers require heuristics that must be justified, etc). Again, this was in a sense "predictable". Starting ~3 years ago it was discovered that McCliece had some yet-unexploited structure, and since then there have been more and more papers exploiting this further, until recently more dramatic attacks have occurred.

In both cases, there is a clear "story" you can (post-hoc) tell about the attacks. You can't always predict precisely where the attacks will end up (for the McCliece attack, it appears more effective than I would have predicted at least). But you can often tell when things are gradually weakening, before a full collapse.

RSA has a cousin (binary characteristic finite field DH) that had this gradual weakening into total collapse happen in the 2010s. It is possible this cousin was a problem child, and GNFS will remain the best attack against RSA until quantum computers fully break it. I can't predict the future. But I can say that ECC has had no such problematic cousins.

This is to say that we are blessed that we have extremely strong cryptography available. Why you would choose to use the weakest defensible option is beyond me, and not something anyone serious about security would ever recommend doing. There is no upside, and only downsides.

2010 is also Citizen's United.

I (and I'm sure others) would obviously agree. just a smattering of the obvious cases

* for years people have noticed that many members of congress use privileged information to pick stocks.

* lobbying post-Citizen's United has a very decidedly "buying politicians" aspect to it

* a congressman (Menendez) was literally arrested while holding gold bars from a foreign government. he went to prison, but is the only person on this list who has iirc.

* the former mayor of new york (a long-time police offer) was embroiled in a Very Funny, very obviously true corruption scandal for turkish airline tickets. the prosecution against him was dropped for no good reason.

the researchers from the RSA-250 record have publicly claimed that factoring 1024-bit RSA keys is within reach of nation states. Your 1024 bit key is only "fine" because you are a small fry, not because cryptographers think it cannot be attacked. This would be true if you used a (non-standard) RSA-768 parameterization as well, which is easier than what we are talking about on this post.

It's also worth mentioning the main concern for RSA is not GNFS, but something stronger. SOTA RSA attacks (such as GNFS) use "index calculus". You can also use index calculus to attack finite field diffie hellman. In the 2010's, there was remarkable progress in index calculus attacks against finite field DH in the small characteristic case. For example, the current record for binary characteristic finite field DH is ~30k bits (and this is by an academic --- a nation state could definitely do more).

It is not known that similar progress is possible in other cases (such as for RSA). But it's very much possible that factoring is much easier than expected. Simultaneously I wouldn't personally bet money on it, and if that breakthrough happened, there were sufficient warning signs that I would feel justified in saying "told you so" to people trusting RSA.

faster hardware could also mean gpu/asic/etc.

I also doubt this is leveraging a lean4 kernel bug, but I also do not think that a 13m LoC proof that has not been human reviewed closes the book on our understanding of Fermat's Last Theorem, in part because of the decided possibility of a kernel bug being used somewhere in those 13m lines.

as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...

not really. it's one of the most difficult ones so far for sure, but pales in comparison to something like the classification of finite simple groups.

This was initially "completed" in the 80s. You can see the timeline for cleaning up the proof in e.g. this mathoverflow answer

https://mathoverflow.net/questions/114943/where-are-the-seco...

it's something that some people have been waiting decades for, and is not yet completed.

note that this is exactly analogous to an LLM being able to slop code some demo, but not build something more generally useful/maintainable (say something suitable for inclusion in a standard library).

it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.