skybrian's recent activity
-
Comment on Beating the frontier on NetHack in ~comp
-
Beating the frontier on NetHack
0 votes -
Comment on The tech industry is investing in mega gas plants to power their data centers in ~enviro
skybrian Link ParentThere are natural gas “peaker” plants. They’re relatively cheap to build so they make sense for occasional use. There isn’t enough data in the article to understand what kind of natural gas plants...There are natural gas “peaker” plants. They’re relatively cheap to build so they make sense for occasional use.
There isn’t enough data in the article to understand what kind of natural gas plants these are and how they compare to others.
-
Comment on The tech industry is investing in mega gas plants to power their data centers in ~enviro
skybrian LinkThis is carefully worded. "Carbon pollution," not pollution. In other respects, coal is a lot dirtier. Not necessarily full time though. Natural gas plants can serve as backup for alternative...Just two gas projects Amazon recently signed on to, which would power planned data centers in Texas and Pennsylvania, would produce more carbon pollution than the dirtiest facility in the country, the giant James H. Miller Jr. coal plant in Alabama that powers 1 million homes.
This is carefully worded. "Carbon pollution," not pollution. In other respects, coal is a lot dirtier.
Once billions of dollars are invested in a gas plant, Guidi said, it is likely to keep running for at least a generation or two, even if the customers it was built to serve ultimately move on to other technologies. “There is a very strong incentive to keep using it,” he said
Not necessarily full time though. Natural gas plants can serve as backup for alternative energy. A carbon tax, which could just be on data centers if it's easier to pass, would change the incentives, encouraging them to use solar or wind when possible (because it's cheaper) and keep the natural gas plants on standby most of the time.
-
Comment on “…and the proof is checked in Lean” in ~science
skybrian (edited )Link ParentOnce a person or organization reaches a certain level of fame, publicity works differently. Like some celebrities, OpenAI will make the news for much of what they do whether they like it or not....Once a person or organization reaches a certain level of fame, publicity works differently. Like some celebrities, OpenAI will make the news for much of what they do whether they like it or not. Things that wouldn’t be newsworthy if some other company did them will be newsworthy because it’s OpenAI. Often that publicity will be negative for OpenAI because people are suspicious of them. They usually can decide whether to make something public (unless it leaks), but they don’t get to control what publicity they get. This is up to all the people outside OpenAI who obsessively follow what they do and write about them.
So no, getting talked about isn’t much of achievement for them, because keeping a low profile is no longer an option. A blog post and a github repo is pretty much the bare minimum to be considered published at all.
The way they did this release shows that they don’t really care about the mathematics community. They dumped work in progress, whatever they had. It’s rude to show that they could publish in top journals in mathematics and win the top prizes of mathematics, but they cannot be bothered to do it right.
So this is like someone rich going to a poor community and doing a money drop, because they can. Rude, tacky, but not unethical. It’s technically a donation. OpenAI apparently used unsolved mathematics problems to test their AI, and they posted the results because, though they don’t really care about the math, other people do. it’s better than not publishing at all, but only marginally so. So, high-status mathematicians have to dig through what they threw over the wall, because this data dump, though done badly, is just too valuable from a mathematical point of view.
The people who say everything OpenAI does is marketing haven’t really come to grips with the inequality of media attention and the consequences of that. Attention that other company’s marketing departments would do just about anything for comes to them for free, and we are a small part of the process that makes that happen.
I suppose it’s true that everything OpenAI publishes is marketing, but often involuntarily. It would be publicity whether they wanted it or not.
-
Comment on “…and the proof is checked in Lean” in ~science
skybrian Link ParentPeople misunderstanding what OpenAI did is inevitable because people who dislike them feel free to make up whatever shit they like about them. Your bizarre analogy is an example.People misunderstanding what OpenAI did is inevitable because people who dislike them feel free to make up whatever shit they like about them. Your bizarre analogy is an example.
-
Comment on AI helps unlock discoveries hidden in Kurt Gödel's notebooks in ~science
skybrian LinkFrom the article: [...] [...] [...] [...]From the article:
Since 2017, the Finnish logician Jan von Plato has led a project at Helsinki University to understand the contents of 16 notebooks that Gödel wrote in the early 1940s. This material – the “workbooks” – is 1,009 pages of densely written text about maths and logic. Much of it is written in a German shorthand, Gabelsberger, that was obsolete even when Gödel was using it.
Progress in the mathematical understanding of the text was painfully slow – about a page a week – until September, when von Plato enlisted the help of the AI model Claude. Within a couple of days, Claude had provided a comprehensive digest of the entire material, revealing Gödel had proved hundreds of theorems that no one knew about.
[...]
In August, at a conference in France about AI and theorem proving, von Plato met computer scientists who suggested that he co-opt the help of Claude in trying to make sense of the workbooks. On his return to Helsinki he began the process, showing Claude his transcriptions of the workbooks, as well as six books he had previously written on Gödel and other secondary scientific literature.
“In a couple of days, I got to see a 650-page explanation of the workbooks. It had to be controlled page for page, but it’s basically a work that is impossible to do for human beings,” he said. “Humans read one page at a time and we tend to forget things. It takes us a year to read about 50 pages. We just are not able to keep in mind all the different parts.
“The AI can connect all the pieces in a thousand pages. It can see all of Gödel’s writings as one piece.”
[...]
Gödel reacted to Cohen’s Fields medal by saying that he had already proved the result in the 1940s. Yet when pushed for a proof by his peers, Gödel was unable to reconstruct one from his notes.
The first task von Plato set Claude was to discover if Gödel’s workbooks had a proof of the independence of the axiom of choice, which would reveal that Gödel had been telling the truth in 1966. The answer came back: yes, almost. “He was just one step away,” said von Plato. “There’s one definition that Gödel got wrong, but he had the right definition two years earlier, and so the thought is that he would have arrived at the right definition anyway if he had just continued for a few months. For me, the architecture of his proof is just wonderful. It makes all of these results of set theory follow a uniform pattern.
[...]
Von Plato said that when Claude presented him with the reconstructed proof of the independence of the axiom of choice, he ran it through the proof assistant Coq, a program that verifies the validity of mathematical proofs, and it passed. Von Plato believes that had Gödel published his work on the axiom of choice, he would have won the 1940 Fields medal. “Maybe he felt that when Cohen got the medal, that that was something he sort of missed.”
In further discussions with Claude, von Plato asked the AI model to extract all theorems in the workbooks for which Gödel either had a proof, had sketched a proof or had an idea for a proof. Claude found 663. When these results were put into Coq: “About 400 were verified as stated, about 200 were repaired, meaning that perhaps the statement of the theorem had to be made more precise, or some assumption had to be added. About 50 were false, and this is no wonder. Gödel himself, when rereading his notes, would occasionally add a marginal remark: falsch! [incorrect] or schlecht! [bad].”
[...]
Hamkins said: “The fact that there are things in there that resemble [Cohen’s proof] does not mean he had it. It shows he was on the path. You don’t get credit for work you don’t tell anyone about. But Gödel had so many ground-breaking ideas that it is maybe not surprising that his notebooks are full of exciting things.”
-
AI helps unlock discoveries hidden in Kurt Gödel's notebooks
30 votes -
Comment on “…and the proof is checked in Lean” in ~science
skybrian LinkFrom the article: [...] [...] [...] [...]From the article:
This post is an attempt to explain in simple terms how to interpret claims of the form “this theorem is correct because it was checked in Lean”. The summary is: there is an important signal that can be extracted from Lean code, but if this code is AI-generated then you need to do some tests first. We explain the tests, and note that in many cases (such as the OpenAI theorem dump) these tests have not yet been systematically done.
[...]
It is worth noting that of the 290 OpenAI theorems which come with Lean code, around 38 of them have the property that the Lean code does not even state, let alone prove, the main theorem of the paper. And OpenAI never claimed that it did! They just said “here is some Lean code which goes with this paper”. Sometimes the code just states and proves some intermediate results — my impression is that OpenAI decided to go live when some of the formalizations were incomplete, so just dumped what they had. To give a concrete example: paper 194 claims to prove Lech’s multiplicity conjecture in commutative algebra, with no restriction on dimension, residue field or characteristic; this question has been open since 1960. The headline theorem in the corresponding Lean code can be checked to be Corollary 5.4 of the paper — already an impressive achievement, but not the headline result.
[...]
When Anthropic formalized a proof of Fermat’s Last Theorem in Lean, they asked me to take a look at the 13 million lines of code which they had generated. I downloaded it onto my machine, dumped it into a sandbox (because who knows what AI-generated code will do, it can in theory delete all your files) and attempted to compile it; I very quickly ran out of memory. I told Anthropic that I was unable to make any claims about what they had done until I could see the code base compiling, and they gave me temporary access to a machine with 96 cores and 500 gigs of ram. I could then compile the code.
Of course, with a more reasonably-sized codebase it is possible to compile the code on a reasonably-sized machine. For example OpenAI’s resolution of the Navier-Stokes problem is 640K lines of code and compiles fine on my laptop.
[...]
Even if the Lean code compiles and passes all these tests, and is thus overwhelmingly likely to be a correct proof of a theorem, this does not mean that any corresponding pdf also contains a correct proof! The Navier–Stokes lost in translation paper demonstrates the opposite in fact, for the Navier-Stokes write-up; whilst all the tests above have been run for the Navier–Stokes work, there are instances where the pdf proof and the Lean proof diverge. In these cases, who knows if the pdf proof is OK! My understanding is that some experts have been using AI to informalise the Lean proof back into English in order to read the argument, rather than ploughing through the slop in the pdf.
[...]
“It’s true because it’s checked in Lean” can be made to make sense. But one has to do some work beyond “the Lean code compiles”. Your frontier AI model can do all of this work. But it needs to be done, and (depending on the amount of Lean code in the proof) it may be computationally costly.
-
“…and the proof is checked in Lean”
28 votes -
Comment on The underappreciated political importance of "everywhere millionaires" in ~society
skybrian LinkFrom an opinionated blog post by the authors of The Everywhere Millionaire. (The book is based on their research. I previously posted a link to a review of their book in the New Yorker.) [...] [...]From an opinionated blog post by the authors of The Everywhere Millionaire. (The book is based on their research. I previously posted a link to a review of their book in the New Yorker.)
Consider a few examples of what we mean. In “Oligarchy and the Great Evasion,” Krugman wrote:
The large majority of U.S. businesses are in fact pass-through businesses, and it’s fair to say that most of them aren’t “real” businesses like, say, car dealerships or restaurants. They are, instead, basically legal fictions created for tax purposes.
Most businesses in America are pass-through businesses. They account for nearly half of employment. Their industrial mix is far more representative of the American economy than traditional corporations. This statement reflects a failure to appreciate how much the structure of American business has transformed since the 1980s.
Moreover, as we have shown in our research and in our book, auto dealers and restaurants are some of the biggest generators of top pass-though profits in the economy. In fact, auto dealers are number 3 on our rankings of 4 digit pass-through profit generating industries with top-1% owners.
[...]
We agree with Krugman that the recent rise in billionaire wealth has been dramatic. But it’s important to put the scale of Forbes billionaire growth into perspective with the other rich and powerful actors in American society. Even at the very frothy public market valuations of the current moment, the Forbes list amounts to around $8 trillion or roughly 4.3% of total household wealth. Meanwhile, based on the most recent SCF, Everywhere Millionaires are probably worth more than $63 trillion or 38% of total household wealth.
Likewise, we are not aware of any Everywhere Millionaires who have the power to shut off internet on the front lines in Ukraine. Scrutinizing economic and political power deployed in antidemocratic ways is an essential public service.
But let’s not blame every policy failure on a small number of billionaires, and, in doing so, absolve everybody else responsible for fixing our current policy problems. The power to legislate still resides with the Congress. The power to regulate many markets is reserved for the states and localities within them.
[...]
Elon didn’t want the massive tax cuts in the OBBBA extended, which did not go to the tech billionaires. He didn’t benefit from the reduced EV demand, which came when the EV credits were abolished. He benefitted little from the new deduction for car loan interest passed in that bill, since financing car purchases is a small part of Tesla’s business.
Who drove these changes and reaped the rewards? The Everywhere Millionaire car dealers who reside in nearly every Congressional district and represent many of them directly. Elon lost big in the midterm election, despite spending half a billion dollars. Meanwhile, dozens of Everywhere Millionaires will return after the election to the new Congress and to state and local government positions across the country.
-
The underappreciated political importance of "everywhere millionaires"
9 votes -
Comment on Data centres have become a dirty word and a political issue in much of the world – has Sweden made one we can all love? in ~tech
skybrian (edited )Link ParentThis is caused by being in too much of a hurry. Big Tech has been building huge data centers for at least twenty years and it wasn't an issue before. Google, at least, was making good progress on...This is caused by being in too much of a hurry. Big Tech has been building huge data centers for at least twenty years and it wasn't an issue before. Google, at least, was making good progress on being carbon-neutral. They funded (and still fund, via investment and advance-purchase agreements) many alternative energy projects.
But due to the AI gold rush/arms race, now everyone including Google is in a huge hurry to build as many as they can, as quickly as possible. So they do whatever they can to reduce the time to build them, and sometimes that means natural gas turbines and taking old power plants out of retirement.
Data centers aren't fundamentally bad for the environment, because they run on electricity and their main inputs and outputs are immaterial. They can easily run on green energy and there are multiple ways to cool them. It's a much easier problem than converting the airline industry to use green energy (for example). Done right, it can also be better for the environment than farming.
Therefore, the goal of regulation should be to slow things down and do things the right way. For example, a stiff carbon tax on electricity used by data centers would encourage them to use green energy even if it takes longer, and to upgrade data centers currently using natural gas to something greener.
It's also true that data centers don't employ many workers once they're up and running. In a way, that could be seen as good, since it allows rural areas to stay rural, instead of turning into suburban sprawl. And because they're so profitable, they can be a good source of local tax revenue. That's a matter of governments negotiating good deals with tech companies in return for having permission to build.
It's easy to get people to oppose things, but it would be better to convince them that there can be local advantages to this trend. It requires smart negotiations to make sure the local community benefits rather than being taken advantage of.
But in an era of widespread skepticism and distrust, how can a community's government representatives gain the trust needed to do the negotiations? It requires the community to trust that they're both smart and honest.
-
Comment on Big balk: On Big Walk, Independent Games Festival, and the present unpleasantness in ~games
skybrian (edited )Link ParentPerhaps the reason we disagree is that, having used LLMs for coding a fair bit, I don’t really buy that what you’re describing is possible. I don’t think we’ve gotten to the point where anyone...Perhaps the reason we disagree is that, having used LLMs for coding a fair bit, I don’t really buy that what you’re describing is possible. I don’t think we’ve gotten to the point where anyone could come up with an innovative, fun to play, award-winning game without talent. The AI tools I’ve used can come up with a working demo and that’s pretty impressive. But the UI will have a lot of things wrong with it and there will be plenty more work to do to make something good.
So, I would still be impressed by the talent of a game developer who used AI to make a game that’s actually good, versus something that’s obviously slop. I would consider it a sign of talent and I’d be interested in knowing more about how they managed it. Maybe it’s not the same kind of talent as developers who don’t use AI, but they clearly know something. I’d be interested in seeing the results of competitions where you’re explicitly allowed to use AI.
I also don’t think using AI should be considered “not making an indy game.” That seems like a retcon. The word “indy” is a bit vague, but it seems like it’s about not having the financial backing of a large game studio. Using AI should allow indy developers to make more ambitious games, but it would still be in service of fulfilling the artistic vision of a few people without major funding.
Also, I think indy developers should be able to take advantage of new technology as it comes available, and I’m interested in seeing how they take advantage of new tools.
-
Comment on Big balk: On Big Walk, Independent Games Festival, and the present unpleasantness in ~games
skybrian Link ParentThis is insider knowledge that I had never heard of. How many people knew these things were hard when the games came out? It seems like you’d need to know the technology’s limitations pretty well,...This is insider knowledge that I had never heard of. How many people knew these things were hard when the games came out? It seems like you’d need to know the technology’s limitations pretty well, and many gamers would just have fun playing the game.
-
Comment on Big balk: On Big Walk, Independent Games Festival, and the present unpleasantness in ~games
skybrian Link ParentFor me the question is why AI is being singled out versus the many other labor-saving tools that game developers could use. This isn’t like journalism where manipulating photos in Photoshop could...For me the question is why AI is being singled out versus the many other labor-saving tools that game developers could use. This isn’t like journalism where manipulating photos in Photoshop could misrepresent the truth. It’s also not like a sports event where everyone agrees on artificial limitations to make the competition interesting. There isn’t even a performance aspect to it, like in music where sometimes we’re interested in what musicians can do by actually playing their instruments.
You should be able to use all the computer graphics you want when making a game, using any tool, just like you can use whatever trickery or special effects you like when making a movie. it’s mostly fake anyway and the “talent” is how good you are with whatever tools you like to use, not what you could do unaided.
-
Comment on NVIDIA reportedly preparing to fire Jensen Huang in ~tech
skybrian Link ParentNVIDIA's stock price is down a fair bit but I don't see why that would cause a crash? Would the next CEO change NVIDIA's strategy in a way that people will notice?NVIDIA's stock price is down a fair bit but I don't see why that would cause a crash? Would the next CEO change NVIDIA's strategy in a way that people will notice?
-
Comment on Scientists study thousands of giant space shades to cool Earth in ~space
skybrian Link ParentWe could also relax fuel regulations to allow ships to go back to emitting more sulfur dioxide, which was countering global warming until recently. https://www.nature.com/articles/s43247-024-01442-3We could also relax fuel regulations to allow ships to go back to emitting more sulfur dioxide, which was countering global warming until recently.
-
Comment on California’s utility wildfire liability conundrum could put clean energy projects in a delay doom loop in ~enviro
skybrian Link ParentYour argument for nationalizing them seem to be imagining a fantasy federal government, one that’s “open and transparent, and average citizens will have a way to be heard in a way they are not...Your argument for nationalizing them seem to be imagining a fantasy federal government, one that’s “open and transparent, and average citizens will have a way to be heard in a way they are not currently heard.”
But in the real world, we still have the Trump administration to deal with.
Even assuming the next president is a Democrat, there’s no particular reason to expect that they would do better than California at regulating a California utility. Stories about poor management at PG&E don’t actually show that the federal government would do a better job. Maybe they would be negligent too?
By the way, some cities in California do have their own public utilities. I thought Alameda Power & Telecom did a decent job when I lived there. More cities handling local electricity delivery themselves might be nice, but it wouldn’t help with delivering power state-wide.
-
Comment on Weekly US politics news and updates thread - week of November 9 in ~society
skybrian Link ParentWhat did these businesses actually do? Did they do anything to start a dispute with the cyclists? If the cyclists were starting a conflict with people who previously had nothing to do with them,...What did these businesses actually do? Did they do anything to start a dispute with the cyclists? If the cyclists were starting a conflict with people who previously had nothing to do with them, I’m not sure free speech rhetoric is enough to justify that, morally speaking.
From the article:
[...]
[...]
[...]
[...]
[...]
[...]