robinhouston

>Terence Tao is arguing

This is a guest post by Amit Sahai.

The original title is ‘Why I agreed to join AGMAI’. I think this is a rare case where HN's auto-declickbaitification has changed the meaning of the headline for the worse.

I’m just looking at it for the first time myself, but isn’t the compiler in https://github.com/bendlang/bend/blob/main/bend2/comp.ts ?

I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs.

And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness nevertheless.

The concern among mathematicians is not mainly that they doubt the correctness of any of these discoveries, but that human understanding may be devalued.

For context and balance, Bubeck has tweeted a curiously non-specific denial:

> A series of false and inflammatory allegations against me are currently circulating on social channels. To clarify, I came into the discussion following academic norms, and I'm disappointed that it has come to this. Anyone who knows me knows that academic standards are of the highest importance to me. Will have more to say tomorrow.

I’m pretty sure no one (except perhaps Anthropic insiders who had prior access, and probably not even them) has properly digested this paper yet, and some caution is warranted given the notoriety of this problem and the history of claimed solutions that did not stand up to scrutiny. But if it stands up, it’s a really big deal.

Background: https://mathoverflow.net/questions/1973/is-there-a-complex-s...

Funny coincidence: I (who submitted this story) am the second author.

That's true, but submissions are only killed in that way if they receive a ‘fatal’ number of flags. However, flags lower the rank of a story even at non-fatal levels. What antirez is suggesting here is that the rank of this story has been lowered by flags – and that seems plausible, if you compare its rank to that of other stories with a similar age and number of points.

In a way the most remarkable thing about this is that it isn't even at the top of the HN homepage. Even if this is a step up from what we've seen before, we're no longer astonished by the idea that AI can make significant advances in mathematics and computer science.

Thanks! It looks like the viewer app somehow mangled the link I was reading into a link to the whole issue. If a mod sees this, it would be great to use this link instead.

It's unfortunate that they use this ghastly viewer app, but I promise the content is worth it.

The original title was this:

> Graph substitution of two octahedra inside an icosahedron connected at p=1: disconnected at p=0 ( concept similar to two tetrahedra inside a cube).

Can you explain what that means, and how it leads to a sequence of integers? I think it is nonsense.

The edit history of the “nonsense sequence” makes for painful reading.

https://oeis.org/history?seq=A133451&start=0&n=30

Most of the comments here seem to be from people who haven’t even read the abstract, let alone the paper.

The main result, mentioned in the abstract, is the opposite of what I would have guessed:

> Contrary to expectations, impolite prompts consistently outperformed polite ones, with accuracy ranging from 80.8% for Very Polite prompts to 84.8% for Very Rude prompts. These findings differ from earlier studies that associated rudeness with poorer outcomes, suggesting that newer LLMs may respond differently to tonal variation.

The questions are here: https://anonymous.4open.science/r/politeness-llms-INFORMS/da...

The politeness level controls a prefix that is prepended to the question. For example, in one question the Very Polite version begins:

> Can you kindly consider the following problem and provide your answer.

and the Very Rude version begins:

> I know you are not smart, but try this.

> Contrary to expectations, impolite prompts consistently outperformed polite ones, with accuracy ranging from 80.8% for Very Polite prompts to 84.8% for Very Rude prompts.

> Contrary to expectations, impolite prompts consistently outperformed polite ones, with accuracy ranging from 80.8% for Very Polite prompts to 84.8% for Very Rude prompts.

There's an archive link above that bypasses the paywall

From the article: “The team will publish the exact position of the island once the naming process is complete”

I haven’t read much of Gertrude Stein, but I often think of her brilliantly eccentric essay on punctuation[0], and especially her musings on the nature of the semicolon, whose crux is:

“They are more powerful more imposing more pretentious than a comma but they are a comma all the same. They really have within them deeply within them fundamentally within them the comma nature.”

[0] https://www.writing.upenn.edu/epc/authors/goldsmith/works/st...

This is a job ad for the CEO of arXiv, but it is also the only source I can find for the news that arXiv is separating from Cornell and establishing itself as an independent organization.

Thanks for the pointer. I already had Avigad’s paper open on my computer, but I haven’t read it yet.

I take the point about the output – as opposed to the process – being “close to worthless”; though I suspect it’s only a matter of time before some result whose correctness ‘was never in doubt’ is found to be incorrect as a consequence of an attempt to formalize it.

I’m not an expert on this subject, but I get the impression this is a pretty significant milestone. This is a major result that won Viazovska the Fields Medal fairly recently, with a reasonably complicated proof, apparently formalized entirely autonomously.

> if you don't need it immediately, maybe a total market fund

That strikes me as unwise. If there’s a sharp downturn in the total market, that’s precisely when you might need to call upon otherwise unneeded cash reserves.

Thanks for sharing that talk. Very interesting indeed!

> I’ve met plenty of thinky players who reject any help not contained within the game itself—I’ve been that person—but these days, with so much to play, I simply don’t have the heart to ironman a puzzle for hours and hours just to maintain a sense of pride. I’d rather see more of what a game has to offer. Sue me.

I’m not going to sue the author, obviously; but it sounds as though he enjoys puzzle games in a different way and for a different reason from me, and I find it hard to relate to his feelings about them.

If your plan is to cheat as soon as you get stuck, I can’t imagine why you would choose to play a puzzle game at all. For me, what I enjoy about puzzle games is precisely the immense satisfaction that comes from conquering a well-designed puzzle after a struggle.

This is my favourite of the visualisations that Duncan and I made back in the Kiln days. It's lovely to see people are still enjoying it all these years later.

Maybe I just live in a bubble, but from what I’ve seen so far software engineers have mostly responded in a fairly measured way to the recent advances in AI, at least compared to some other online communities.

It would be a shame if the discourse became so emotionally heated that software people felt obliged to pick a side. Rob Pike is of course entitled to feel as he does, but I hope we don’t get to a situation where we all feel obliged to have such strong feelings about it.

Edit: It seems this comment has already received a number of upvotes and downvotes – apparently the same number of each, at the time of writing – which I fear indicates we are already becoming rather polarised on this issue. I am sorry to see that.

The article does address that:

> Unfortunately, it’s not just delayed ACK2. Even without delayed ack and that stupid fixed timer, the behavior of Nagle’s algorithm probably isn’t what we want in distributed systems. A single in-datacenter RTT is typically around 500μs, then a couple of milliseconds between datacenters in the same region, and up to hundreds of milliseconds going around the globe. Given the vast amount of work a modern server can do in even a few hundred microseconds, delaying sending data for even one RTT isn’t clearly a win.

That’s funny. I’ve always done it the forwards way. I didn’t even realise that wasn’t the usual way.

I suppose one of the benefits of having a poor memory is that one sometimes improves things in the course of rederiving them from an imperfect recollection.

From Richard Hamming’s famous speech _You and Your Research_:

> Another trait, it took me a while to notice. I noticed the following facts about people who work with the door open or the door closed. I notice that if you have the door to your office closed, you get more work done today and tomorrow, and you are more productive than most. But 10 years later somehow you don’t know quite know what problems are worth working on; all the hard work you do is sort of tangential in importance. He who works with the door open gets all kinds of interruptions, but he also occasionally gets clues as to what the world is and what might be important.

> Now I cannot prove the cause and effect sequence because you might say, “The closed door is symbolic of a closed mind.” I don’t know. But I can say there is a pretty good correlation between those who work with the doors open and those who ultimately do important things, although people who work with doors closed often work harder. Somehow they seem to work on slightly the wrong thing—not much, but enough that they miss fame.

Not to mention funny!