mswphd

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.

junk theorems aren't the concern, soundness issues in the lean kernel are the concern.

Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.

As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals

https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".

if you do want to do local LLM stuff, mac studio is significantly better than most linux dev boxes.

In general you don’t need things that fancy. Instead, you can take

1. Some known set of architectures, with

2. Some known set of (constant time/variable time) operations

And then prove things about programs written against those architectures. See for example

https://github.com/PLSysSec/FaCT

That being said, practically the operations that are variable time are known, and are mostly* the same on all modern architectures. In particular

1. Branching on a secret-dependent variable, or

2. Indexing an array with a secret-dependent index, or

3. Some architecture specific operations (typically things like division, occasionally things like multiplications/shifting).

someone tried doing this for rust, but the reaction was that it was vibe-coded/low quality.

https://github.com/rust-stdx/stdx

https://news.ycombinator.com/item?id=48571266

Note that there are baby versions of this that are uncontentious, for example

https://blessed.rs/crates

this is missing the LTS release. but it is a curated group of libraries that are relatively uncontentious to recommend.

misspoke, meant rim brake bike

only real worry I'd have is a scenario like

1. someone has a cheap disc brake bike for pleasure rides (mostly in the sun)

2. they get something like this for commuting or whatever

3. now they're on their disc brake bike most days (including when it rains), going faster than they're used to

it's not the end of the world, but it also doesn't seem great

it's also likely mildly more dangerous than a standard ebike, as ebikes typically overprovision their brakes. A customer putting this on a standard bike (especially a disc brake bike) might have less stopping power than they want on an ebike.

ASUS does make power banks, and the vast majority of the cost of any ebike is in the battery.

only temporarily, and only for multiplication. At a very high level, the idea is that you view C := [A, b] as satisfying

CS = 2^8 m + e

here, S = [-s, 1] is a padded version of the initial secret. So recast everything as a linear equation (matrix) equation

CS = 2^8m + e

Without getting into too much details, one can define a "product" * such that

(CC)(SS) = (2^8m + e)(2^8m + e)

This becomes a "degree 2" equation. Mildly faking the details for simplicity, one can expand it out not in terms of A, b, but in terms of three components A, b, c, where c is the "degree 2" component. So here things have inflated. But there is also a technique to shrink this back down to a linear equation.

This shrinking process requires some auxiliary data, namely an encryption of SS under S. it is not the problematic part of HE though. Instead, data movement (say a circular rotation by k indices) also requires some "fixing up", though here involving an encryption of rot^i(S) under S.

This is more problematic, as there are many different rotations (often on the order of thousands), and you naively need a piece of auxiliary data for each of them (vs one for multiplication). There are ways to shrink the required number of keys, but in general they're the "heavyweight" part of FHE.

the basic encryption scheme used here is fairly straightforward actually, at least the symmetric encryption version. Let s be a uniformly random, 512-dimensional u32 vector. To encrypt a message m (say a 512-dimensional bit vector for simplicity), you

1. generate a 512 x 512 random (u32) matrix A, and

2. generate a 512-dimensional rounded (to the nearest integer) Gaussian, say of standard deviation 10, e.

The ciphertext is then [A, b :=As + e + 2^8 m].

To decrypt, you compute b - As to recover 2^8 m + e. You can then recover m, as e << 2^8 with high probability.

Anyway, if you have two of these ciphertexts, you can sum them together to get

[A1 + A2, (A1 + A2)s + (e1 + e2) + 2^8 (m1 + m2)]

this decrypts to m1 + m2, so you can recover homomorphic sums (or scalings by small integers).

Multiplication is more complex, so I won't get into it here. But the high level from the above example is that you could have someone compute arbitrary linear functions of your data without them knowing what your data is.

conceptually your example is fine/good, but it's worth clarifying that the scheme you describe is insecure, as unpadded RSA fails to be IND-CPA secure. this is because Enc(m)Enc(m') = Enc(mm') is a predicate a passive observer can check, to gain information about Enc(m*m').

that being said, you can construct IND-CPA secure homomorphic encryption schemes from factoring-based assumptions iirc, so this isn't a fundamental obstacle.

SOTA for SVP is BDGL16. You can find discussion of it in many places, see for example

https://eprint.iacr.org/2022/922.pdf

it's hard to precisely analyze BDGL16, but to leading order it takes ~ (3/2)^n time, which is roughly 2^{.292n} time.

When I say it takes roughly this amount of time, this is likely modulo several heuristics. With the caveat that I'm not a lattice cryptanalyst, my understanding of the heuristics is the following. BDGL16 is a "sieving" algorithm. To find a short vector v, you

1. start with many long vectors v1, ..., vn.

2. take their pairwise differences. this may produce shorter vectors (and if vi are suitably randomly distributed, this is provably true).

3. repeat

there are other tricks on top of that you do, but that's the conceptual core. As I mentioned, if the

1. initial vi were suitably randomly distributed, and

2. you could prove the pairwise differences were also suitably randomly distributed

you could likely get a provable running time bound on things. At least the 2nd likely breaks down (maybe the first as well though), so you instead only get a running time bound under the above 1+2 heuristic assumptions. In cryptanalysis this is typically viewed as good enough, as long as the heuristics are solid (for example, SOTA for factoring, the Number Field Sieve, only has heuristically understood running time iirc).

This paper is instead about provable algorithms. They can be conceptually interesting, and useful if there is not community consensus that the heuristics are solid. But in lattice cryptography everyone thought BDGL16 used reasonable heuristics, so SVP took 2^{0.292n} time practically, even if it was too difficult to formally prove this.

that's the running time of the BDGL16 sieve. see the intro of e.g.

https://eprint.iacr.org/2022/922.pdf

for some history

the server doesn't do what you say. Roughly, the server has a fixed circuit C they run on the ciphertext. They run this same circuit on any ciphertext. They give you back the result. the fact that the result, when decrypted, gives the desired answer isn't something the server can verify though.

Think about a very simple setting, say a database lookup. I send an index `i` in a database I want to lookup. The server sends back DB[i] or whatever.

In the clear, the server can immediately fetch the correct row. Under FHE, the server does a full scan of the database, and (roughly) for each row will do something like DB[i] * (encrypted selector variable that is 0 or 1 depending on if it is the row you want).

This is actually a baby version of FHE known as "Private Information Retrieval". For it, you (roughly) can design an encryption scheme that supports linear function evaluation. For example, a ciphertext Enc(m) can be paired with a matrix A to produce Enc(Am). You can then encrypt the ith basis vector m := e_i, and view the database as a matrix DB, to get DB * Enc(e_i) = Enc(DB*e_i) = Enc(DB_i). This works, and can be implemented in ~1k LoC, e.g. it is not particularly complicated to practically instantiate (though this basic sketch has some performance issues).

note that this is even true for an honest server. Roughly, FHE computations often require certain bounds on the (encrypted) messages for things like tuning polynomial approximation domains etc. If your messages are out of distribution for the tuned polynomial approximations you'll get back garbage as as result.

addition is easy/essentially the same cost as standard (not really, because you have to compute mod p addition rather than mod 2^32, but ignoroing that it's roughly the same).

as a general rule multiplication is the difficult part.

it's hard to accurately quantify what "nontrivial" cost overheads are because they're very application dependent. for example, things that require encrypted control flow are very hard under FHE. so an encrypted hashmap sounds roughly unimplemnetable. but things that do not require encrypted control flow (e.g. many ML applications) are less bad. this can still be quite bad though. for example, relu is trivial in plaintext. it is hard homomorphically, because the trivial way to write it uses private control flow.

I've found having draconian phone blocking rules helps. I use Jomo

https://jomo.so

but I'm sure there are other competing products.

Roughly, you can classify apps in your phone to things that

1. are fundamentally fine (various bank/payment apps, messaging app, map apps), and

2. are known time wasters (social media)

you then just block the time wasters. you can configure it so that to edit the settings of the app, you have to enter some 150 character randomized code. it is very annoying to do.

this is the point though. there are other ways you can add friction to using your phone. setting its display to be black and white makes it much less enjoyable to use, for example. if you add in enough friction (and stick with it over an initial "hump"), you'll findi yourself reaching for other options.

OpenRouter is (roughly) a single proxy between you + many different models + providers. it works with opencode (+ many other products), and is relatively convenient for trying out a bunch of models.

for example, they already have qwen3.8-max

https://openrouter.ai/discover?model=qwen/qwen3.8-max

note that they add some fee ontop of things (maybe 10% of spend?). it isn't htat big of a deal for general experimentation, but if you end up wanting to use a single model in a higher-volume way, it likely makes sense to cut them out of your stack.

not really. The hardness of SVP is relevant, but this is a paper giving improved provable bounds for SVP algorithms. heuristically (which people use to choose parameter sizes etc) people assume SVP is much easier to solve, closer to 2^{.29n + o(n)}.

So it's tangentially related, but does not itself imply an improvement on the (heuristically assumed) SOTA for these problems.

it's worth mentioning the infinite number of decimal places isn't an issue. there is the formalism of computable numbers to get around this

https://en.wikipedia.org/wiki/Computable_number

roughly represent each number as a turing machine, which on input i outputs the ith digit. it works fine (it's slower than floats, but that's a different concern).

the issue is that the computable numbers are relatively small. in particular, there are countably many turing machines, so they're a countable subset (in fact subfield) of the reals. so in a precise sense they only make up a vanishingly small fraction of the real numbers. but they still capture many important mathematical constants, e.g. e and pi.

it doesn't overturn much. For example, here is a post from 2004

https://www.math.columbia.edu/~woit/wordpress/?p=105

it is about a purported (though incorrect) positive proof of the Jacobian conjecture in 2 dimemnsions. It is true in 1 dimension. The Fable proof is that it is false in >= 3 dimensions. 2 dimensions is still open.

Anyway, in that post it says

> It now seems that a proof has been found by Carolyn Dean of the University of Michigan, for the case of polynomials in two complex variables *(for more variables, many people believe it is not even true)*

so the resolution of this is a "surprise" in that it is a very long open with many failed proof attempts. But the direction it resolved was not surprising.