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.
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.
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.
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'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 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.
> 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.
> do you expect this to remain true? If so, for how long?
For the foreseeable future. Left to their own devices current LLMs kinda wander off into outsider art territory. They aren’t grounded in the real world and they need that feedback loop to stay within the category of relevant ideas. I haven’t seen anyone working on fixing that.
Regarding 1, the same is true of every other scientific field. Verifying some tidbit of knowledge for yourself as an individual isn’t optimally useful in all circumstances.
Regarding 2, if the proof isn’t understandable then it probably isn’t useful. Many people today work in the hypothetical world where the Riemann Hypothesis is true, and many work in the hypothetical world where it is false. If it takes decades to validate that some horrifically complex AI proof of either fork is true, people will probably continue working on the other fork just in case.
> For the foreseeable future. Left to their own devices current LLMs kinda wander off into outsider art territory. They aren’t grounded in the real world and they need that feedback loop to stay within the category of relevant ideas. I haven’t seen anyone working on fixing that.
I have. DataAnnotation and these other AI-training piecework companies are pretty much the backstop now against total navel-gazing model collapse. With the Dead Internet Theory now pretty much reality, it's not like there is, or is going to be, gobs of untainted human-generated data out there ripe for the harvesting so it's going to take active human effort to keep the models grounded. That is, of course, until they start inhabiting robot bodies so they can live and move around in the real world, and thereby achieve their grounding, as in GitS or Ex Machina...
reply