Yes in the sense that users flagged it, but not in the sense that moderators penalized it. I didn't see it until someone emailed a couple minutes ago.
The only thing I've done since then is mark the post so it won't be killed by excessive user flags. This means the thread can stay open for new comments.
I'm not going to remove the flags, because they are clearly an authentic community reaction, though of course some users will have the opposite reaction as well; this is normal.
IMHO, for fairness, upvotes should be the vouches countering the flags. I think unless the amount of flags is really significant, they shouldn't have priority over the 117 upvoters (and counting) who are clearly interested to have this discussion here.
My thinking could be naïve, as the algorithms were probably created with the backing of some data and experience, but anyway, I felt like sharing my opinion.
In a real tug-of-war, the teams are balanced. In the HN tug-of-war, flaggers have an advantage because flagged posts are invisible to people who might otherwise upvote them.
Almost any moderation system working under consistent rules will be stable, because the people and topics disadvantaged by the moderation will simply leave your platform.
I'd hazard that someone is waiting-not-waiting, like Smaug, for a systems quant (bonus: lisper) to enter the cave to do equilibrium teleportation experiments on votes and flags
(I am secretly hoping that this is a silent-smoke-out-of-ears --and not self-extinguishing-- comment)
Flags having a stronger influence than upvoting is a necessary algorithmic check against genuinely bad behavior/brigading, not disagreement. In general it works as intended, which is the best you can do without something potentially worse.
Are there any stats available on the weighting ratios such as flags to upvotes, likes and comments per post after flagging, average time to frontpage to flag?
(G summarises the following[0], but a definitive source would clear up what the necessary algorithmic checks are).
I'm curious - Do you have a reaction to the specfic point of suggestions that were brought to you, per the article? Do you recall specific ones, and if they were considered/deliberated?
I applied it in this case by preventing the thread from getting killed outright, which would have closed it to new comments. This is moderating less than we normally would, since any thread that is flagged this heavily would normally get killed.
It's important to understand that "moderating less" means moderating less than we normally do. It doesn't imply "not moderating at all", and certainly not "always override user flags". Those would be loopholes that any internet provocateur could drive a truck through, as I've mentioned from time to time over the years: https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
Wouldn't excessive/above average flagging rather indicate a post is controversial/counter narrative enough to warrant longer front page exposure? It certainly seems to have gotten the people going in the short time it was up, and it's not a secret that early vocal users can be quite generous with the flag button.
Some community reactions are considered more authentic than others, it would seem.
I’ve seen so many shit articles and corporate announcements manually unflagged by the mods over the years. (Here’s a recent one, flagged to death very quickly before miraculously being resurrected: https://news.ycombinator.com/item?id=49602728) An explanation is rarely given.
I don't have access to the entire article, but it doesn't mean much to physics.
Physicists knew Navier-Stokes was an approximation that breaks down at some scale, e.g. the molecular scale. This AI solution just exhibits such a breakdown.
Unfortunately attaching a corporation name to a statement is a large part of the motivation for a company to spend millions on tokens for Lean proofs. It's a marketing/PR spend for them. Without their name attached, the return on investment is far less.
That said there are some efforts in the direction you're suggesting. For example
- [Prove2Me](https://beta.prove2.me) - Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. One creates open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.
- [Tau Ceti](https://github.com/TauCetiProject/TauCeti) - An AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
Early 80's I learned Logo and Basic at a local store that sold Apple computers. It was called "The Logical Choice" and had a classroom tucked away behind a false wall and an English Sheep dog "Sir Isaac Newton" that would hang around the store!
Nice, I just found a story on the store, page 5 of [1].
Money isn't the issue here, I'm trying to determine if they are able to offer a better value/speed than I can currently extract from renting a 3+ month block of cards myself. Time is a bit more important to me
Maybe in the future mathematicians could be the ones proposing different axiomatic foundations (e.g. ZF vs ZF + C vs ZF + C + CH vs ...) and then using computers to examine the consequences of these differing foundations?
I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been worked out. (The most productive hypothesis has been what's called "projective determinacy", if you're curious.)
Mathematicians have also gone in the opposite direction, and tried to work out what are the weakest foundations where different results hold. This is called "reverse mathematics".
What name does this "well-developed field of mathematics" go by? (I just want to get a taste of what the field is like.)
I also thought that there are an infinite set of possible extra axioms, e.g. axiomize any statement that's true but not provably so via Gödel's First Incompleteness Theorem, though maybe the vast majority of such axioms are "uninteresting".
"Descriptive set theory" is a good starting point, though it's the bulk of what set theorists in general do.
It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that have consequences that humans are interested in fall into simple families. For example, many seemingly unrelated questions are settled by assume the existence of very large sets (larger than can normally constructed in set theory).
Looking a bit more into this, it doesn't seem your claim "most of the consequences of additional axioms have been worked out" holds up.
Yes, metamathematics is well-developed, but I don't think that most of the consequences of any particular additional set of axioms have been worked out. Each such new set requires re-deriving all of this alternate mathematics from scratch. This is a lot of work!
So I think my original claim---mathematicians select interesting axioms and AI figures out their implications---still seems a possible way forward.
PS: I'd guess descriptive set theory under determinacy is the one place where projective determinacy, as you stated, pays off.
I don't see how you came to that conclusion, since I'm telling you the actual state of play. There's a big literature on what results require the Axiom of Choice, for example. (The book Handbook of Analysis and Its Foundations covers this thoroughly.) There are many results on what follows from the Continuum Hypothesis or other cardinal arithmetic axioms. There is a big literature on what follows from assuming the existence of large cardinals. There's a separate literature on adding "forcing axioms", like Martin's maximum. There are hundreds of papers on open questions that are settled by adding additional axioms to ZFC, and to identifying the weakest axioms to add to settle various open questions.
In another direction, there's even a literature on what happens when you allow sets to contain themselves as members, like Aczel's Anti-Foundation Axiom. There's literatures on purely constructive versions of set theory, where everything has to be computable. Like I mentioned before (reverse mathematics), there's work on what happens when you adopt much weaker axiom sets, like second-order arithmetic but weak choice principles such as taking Kruskal's tree theorem as an axiom.
So while AI would accelerate this work, the existing body of work on alternate axioms is tremendous. A surprisingly large amount of it translates between systems, and there are precise tools to measure how weak or strong a system is, relative to its competitors.
While the existing body of work on alternate axioms is tremendous, it's finite. The set of possible axiom systems is infinite. Does current the current body of work cover all consequences of all possible axiom systems?
> I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).
> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.
> We shared the resulting proof with Kevin Buzzard, who said:
> > This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.
It has reached beyond government institutions. From the linked article:
"These policies’ tentacles already extend beyond government websites... Reports say scientists are self-censoring in hopes of improving their chances of getting government grants."
In regards to government institutions, limiting speech in this way will cause people to die.
For example, banning the phrase "air pollution" will curtail efforts to address air pollution, e.g. scientists not submitting research proposals addressing air pollution, causing people to die as a result[1].
Their CEO was in the Obama admin, and they didn't really press Biden/Obama to the same extent with high profile advocacy on whistleblowers, Assange, Espionage Act, etc.
reply