I asked free chatgpt to give me some essays that will fool a slop detector and they all fooled this slop detector. Its best guess was "6% slop probability 87% confidence answered in 0.5 s for $0.000027" and yet it was 100% slop.
I am very skeptical slop detectors will ever work.
> 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.
ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).
zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.
If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.
> when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.
its bro-math. In formal math you need to be specific what inference system you use. There are many of them. Then you need to have formal proof that in that system you can derive concept of function and then think about question if it won't make paradoxes and contradictions with ZFC.
It's a red flag. Even if they agree and understand whatever they copied from chatgpt, they were too lazy to clean up its output. Are they also too lazy to read the news or does chatgpt summarize their articles too? AI people are like emperors without clothes. Totally embarrassing to witness.
This is bad because it's only getting harder to trust people. This is not someone I would want representing me. Although I'm not thrilled about any of my representatives anyway.
That's your handle and it points to the server where your atproto account's data is stored. You can use this same login for other atproto apps and it will all be stored on the server at tngl.sh A username.bsky.social handle just means bsky set up that account and your data lives at the bsky.social PDS. You can migrate to a different PDS and change your handle if you don't trust them. You can host a PDS yourself if you like. I agree it's a little clumsy, but I'm sure friction can be reduced.
The idea is to give users control over their identity, network, and feeds instead of big social platforms like facebook or twitter that choose what content you see and lock you into their closed network.
They made a transphobic joke 3 times and the bluesky users that enabled their intolerance filter never saw it. What exactly is the problem? The posts weren't deleted. Nobody liked the joke because it's a bad joke.
I don't use bluesky, but out of interest is this "intolerance" filter effectively a political filter, or an actual "intolerance" filter?
Like if someone is talking about "white fragility" and being intolerant towards white people, or being xenophobic about American culture, would that be likely to result in them being flagged for intolerance also?
Asking because while I don't mind the concept, I find in practice most of the time platforms add these filters and rules as a way to enforce ideological consensus.
It's dreadfuly simple - Bluesky users can choose what content they want to see - including selecting feeds, algorithms, moderation services etc. This situation is intolerable to people who believe that their right-wing views must be forcefully shoved down users' feeds, because not liking and not wanting to see their shitty content is considered an attack on freedom of speech.
That's not true though. If many people or the mods flag a post, other people cannot see it without clicking - it's covered by a banner. I have a new user on bsky, I never touched any configuration knob and by default I can't see certain posts. Someone decided for me.
If I were truly able to decide what I see I would see every single post as a new user. Then I would have the optuon to opt in to lists, banning / hiding other users etc.
Instead, I'm forcefully opted-in to not seeing what someone else decided I shouldn't see from the start, and I must find the way to opt out.
Didn’t you just say you can click to see it? So you can see it.
It’s hardly any different than those placards they used to put over the swimsuit magazines in the checkout line at the grocery store. No one was stopping you from buying it and seeing all the titties you wanted.
I am very skeptical slop detectors will ever work.
reply