I’m not seeing anything like a falsifiable prediction that LLMs will write math proofs in that article.

I see a thought experiment about giving GPT-2 “near-infinite training data and [compute]” but that’s not falsifiable. That’s also not how we got to modern GPT models.

He's pretty clearly saying he beilieves the technology capable of such a feat, at least in theory, which is far more than many would deign to admit even a year ago, nevermind 7. He had the right idea/model of LLM capabilities, which is more than you could say for a lot of people, even in this very thread.

If that’s your standard for what counts as prediction, Asimov beat him to it by seventy-ish years.

EDIT:

> Scott made comments on a specific emerging technology

He was speculating on what would happen if one gave GPT-2 “near-infinite training data and compute.” It’s a thought experiment, not a prediction. Near-infinite amounts of anything is a fantasy.

I acknowledge that he has predicted some things in a falsifiable way and turned out correct, but this isn’t one of them. You’re reading hindsight into the text.

>I acknowledge that he has predicted some things in a falsifiable way and turned out correct, but this isn’t one of them. You’re reading hindsight into the text.

I read that blog years ago. Believe me, my opinions are not hindsight.

>Incorrect. He was speculating on what would happen if one gave GPT-2 “near-infinite training data and compute.” It’s a thought-experiment, not a prediction. Near-infinite amounts of anything is a fantasy.

Thought experiments can generate predicitons. His claim was essentially: If you scale data and compute sufficiently, this technology can learn enough of the underlying structure of mathematics to write proofs.

This is meaningful when others around you are saying this is a dead end and that the technology is fundamentally incapable of this regardless of degree of investment and scaling. It shows a much better calibrated sense of the potential of the architecture than those who said otherwise.

If your objection is that "near infinite" makes it insufficiently quantitative to count as a falsifiable forecast, then fine. But at that point we're mostly arguing over what deserves the label "prediction" rather than whether Scott correctly identified an important capability the architecture could develop.

And i'm not trying to say this makes Scott (or the lesswrong crowd) geniuses.

1. Asimov wrote science fiction stories. As far as his robots were concerned, he did not make any comments on the possible future direction/capabilities of any specific technology at the time. This meant he could imagine his robots however he wanted for his fictional world. Scott made comments on a specific emerging technology - You can imagine math proof writing robots but be unconvinced they could emerge from Generative Pre-trained Transformers.

2. The genre is alternatively called speculative fiction for a reason. Yes, some sci-fi works do count as predictions especially when hinged on concrete emerging technologies.

Lesswrong people are also scifi writers. Asimov is ji ust more self aware and better writer.

The context shows he was simply whining about AGI skeptics back in 2018, and many of the “predictions” he makes in that paragraph (including the one you quoted) are trivially wrong because he phrased them so hyperbolically and categorically.

Anyway, there were plenty of normies who thought images generated by e.g. stable diffusion (c. 2022) was “real art” and equivalent to human artwork.

I don’t think it’s useful to glaze Scott (or any of the LW crowd for that matter) as if he was (or they were) some kind of prophet(s). They got a couple points right, sure, but most of it was them flinging armchair philosophy spaghetti against the wall and seeing who would fund MIRI to let them fling the next batch.

Okay, fair enough.

I’m inclined to agree. Sometimes when (perhaps other) people say this there’s an undertone of “and the field is full of not-real mathematicians” as if there’s a large contingent just hanging on for the money or prestige, and I personally haven’t seen that in the wild.

I doubt outside of a few exceptional cases that one is going to do better on CPU-bound problems than a well-written LAPACK implementation built for the architecture you intend to run on.

Maybe pedagogy was the point? I didn’t really get that from the article, maybe some intention was lost by filtering it through AI.

Author here. Performance-wise, it will never ever be a serious solver. No matter how hard you try. And for this particular matrix, (2D Poisson, block tridiagonal with tridiagonal blocks, quarter millions unknows), LAPACK isn't gonna do it either unless you take special care.

Pedagogy is indeed the point. This is the 4th (3rd?) post in this Jacobi series. Gauss-Seidel and Jacobi are sufficiently simple that very little math is needed to understand how they work. But they also offer a very nice opportunity to illustrate the interplay of mathematical algorithms and actual hardware implementation as well as gradually introducing some elements of performance engineering.

To give you idea of where we're going: after discussing SOR and make connections with other fields of applied math, we'll eventually get to multigrid solvers. And Jacobi and Gauss-Seidel play a really important role in this. Multigrid are also some of the best iterative solvers possible for such discretized elliptic operators. But I can only blog now and then, and I want to take one step at a time so that upper-level undergradute in either math or computer science can follow along.

LAPACK doesn't do sparse systems.

(On the other hand, I skimmed the article and this might be a banded system, which LAPACK can handle).

Author here. The second-order accurate finite difference approximation of the 2D Poisson operator is a block tridiagonal matrix with tridiagonal blocks. There are ways to handle it with LAPACK, but you'll still need special care. And 512x512 grid points (quarter millions unknowns) really is a toy problem. The linear systems I work with typically have in the billions of unknows, and LAPACK is not gonna cut it no matter how smart you are.

This is the 4th (3rd?) post in this Jacobi series. Gauss-Seidel and Jacobi are sufficiently simple that very little math is needed to understand how they work. But they also offer a very nice opportunity to illustrate the interplay of mathematical algorithms and actual hardware implementation as well as gradually introducing some elements of performance engineering.

To give you idea of where we're going: after discussing SOR and make connections with other fields of applied math, we'll eventually get to multigrid solvers. And Jacobi and Gauss-Seidel play a really important role in this. Multigrid are also some of the best iterative solvers possible for such discretized elliptic operators. But I can only blog now and then, and I want to take one step at a time so that upper-level undergradute in either math or computer science can follow along.

True, 2D Poisson is only approximately banded. Still, I don’t think I’d bother rolling my own sparse solver. It’s a well-trod problem.

Author here. It actually is a block tridiagonal matrix with tridiagonal blocks. The test problem only has a quarter millions of unknowns so, for a production run, I wouldn't bother write my own sparse solver either. Here, it is done mainly for the sake of pedagogy to help students understand the interplay between a mathematical algorithm that looks good on paper and its hardware implementation which is not as promising as one would expect.

Jacobi and Gauss-Seidel wouldn't be solvers I'd even consider for a real problem. But they are simple enough that anyone with a basic understanding of linear algebra and programming can follow along. But much research requires me to run simulations on thousands (if not hundreds of thousands) of cores, and there, off-the-shelf solver implementations will often not cut it.

Various algebras of dual numbers are used in most automatic derivative routines.

This is treated more rigorously and generically in the subject of synthetic differential geometry.

wanted to say this.

Also conceptually it feels just right to use nilpotents to probe the smooth structure. In a way nilpotents are violently smaller than even non standard analysis infinitesimals, as the laters’ powers are incredibly small but never vanishing.

Another way to see this is that it makes Taylor expansion exact by killing terms above a bound so it works naturally with the ecosystem surrounding it

Finally duals are very similar to complex in a way. i can be defined as root of X^2 + 1 = 0 even if it felt impossible initially, the dual number as a non nul solution of X^2 = 0 even if it is as counterintuitive.

I remember learning about that from Stephenson’s Cryptonomicon, back in the day.

It’s not even a US-specific thing. Many countries recruit foreigners to their militaries.

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

I've heard of some people on the lam who wanted to join the French Foreign Legion, a military that gives a no-questions-asked grant of citizenship at the end.

That's not how it works, and I have firsthand experience, and hasn't been for at least three decades. The very first thing that happens when you show up in Fontenay-sous-bois is that they run Interpol checks and other checks in your country of residence or anything notable in your passport.

Gone are the days of accepting any criminal openly.

They do however, if you either complete your contract, or are injured, deem you eligible for French citizenship "by spilled blood".

> Technically a large landmass, but essentially nothing happens in the western half.

Depends what you mean by "western half," I suppose, but China is definitely not a relatively small country. Shanghai to Chongqing is about the same distance as Chicago to Dallas; Beijing to Kunming is about the same as D.C. to Denver.

I hate the dark forest more than just about any scifi trope but reality just keeps proving it right.

I also think the trope is a little overused, but do wonder if there is an interesting analogy for what this will do to research: Massively incentivize keeping results secret, to avoid being scooped by someone willing to throw enormous compute at your partial solution.

So less about hiding civilizations, and more about hiding information. Math is clearly headed in this direction, and I see no reason why the rest of intellectual work shouldn't too.

This is very sad, but I came to the same conclusion with my math blogging a couple years back. There’s little point to publishing any personal effort on the internet anymore. At best you get some spam comments and your work stolen by bot scrapers; at worst you get a doxxed and targeted by a harassment campaign.

My go-to is “It’s the only thing I was good at in school, I was hopeless at everything else,” which is only a slight exaggeration.

> It’s highly nontrivial to verify that a 250k loc Lean program actually represents that which it claims.

Generally you only need to look at 10-100 lines (unless you have a highly novel theorem that essentially invents a new field of math or builds on a field that has never been worked on in Lean before) of the 250k to verify what it claims. This is why there is excitement around formal verification. The rest of it is perhaps useful to read to figure out why the proof works, but is not necessary for checking.

Human verification of the Lean program only requires verifying that the theorem itself is represented correctly. The theorem will only make up a very small part of the entire Lean program.