an explicit Diophantine equation whose lack of solutions is provably equivalent (in PA) to Con(ZFC)
(i'm working on making it smaller, Lean proof is not complete yet)
github.com/VladimirReshet…
(i'm working on making it smaller, Lean proof is not complete yet)
github.com/VladimirReshet…
22
30
299
20,617
Cleo retweeted
@_Mira___Mira_ PA formalization of Halt(215) <-> NOT Con(ZFC): github.com/elliotglazer/k…
Cleo's original post: x.com/ereliuer_eteer…
More on set theoretic reflection:
en.wikipedia.org/wiki/Reflectio…
onlinelibrary.wiley.com/doi/10.1002/ma…
Cleo's original post: x.com/ereliuer_eteer…
More on set theoretic reflection:
en.wikipedia.org/wiki/Reflectio…
onlinelibrary.wiley.com/doi/10.1002/ma…
now 215 states, with Rocq and Lean proofs
i'm working on proof simplification, and showing that it's interpretable in PA
github.com/VladimirReshet…
3
3
14
1,210
some people believe that once a particular 384-bit sequence has been published on the web, true random generators begin disfavoring that particular sequence in the future
3
0
34
2,492
if a key XORed with one of these sequences doesn't look random, does it mean that it was likely not generated by a random process?
does 20be80f1b6895dad611896f854b9dfb58ebd75a2d1869526a610c524de0e5426ba5f89af8a0c51d146ccb39f479ca9ae look random enough to be likely generated by a random process?
does 7650178e7d7ce3fc60521262ada3b88ada55caa4c59fbd6d701577befa3220f814e5eb5c2bd3c6ee6e9d332333ee2871 look random?
0
0
4
974
does 20be80f1b6895dad611896f854b9dfb58ebd75a2d1869526a610c524de0e5426ba5f89af8a0c51d146ccb39f479ca9ae look random enough to be likely generated by a random process?
does 7650178e7d7ce3fc60521262ada3b88ada55caa4c59fbd6d701577befa3220f814e5eb5c2bd3c6ee6e9d332333ee2871 look random?
does 7650178e7d7ce3fc60521262ada3b88ada55caa4c59fbd6d701577befa3220f814e5eb5c2bd3c6ee6e9d332333ee2871 look random?
@ereliuer_eteer @isaac_ts_way Taleb calls this Ludic fallacy: en.wikipedia.org/wiki/Ludic_fal…
If a 384 bit Keys comes out as 4, the most reasonable conclusion is that the key was not really 384 bit.
10
0
20
8,332
now 215 states, with Rocq and Lean proofs
i'm working on proof simplification, and showing that it's interpretable in PA
github.com/VladimirReshet…
i'm working on proof simplification, and showing that it's interpretable in PA
github.com/VladimirReshet…
BusyBeaver(230) is independent of ZFC! I have verified in Rocq that a certain 230-state Turing machine halts iff ZFC is inconsistent. This surpasses the non-formalized 243-state TM of @ereliuer_eteer and the formalized 254-state TM of @_Mira___Mira_.
3
4
37
3,139
folks, don't forget that i'm a troll 😈
but i don't do it for lulz, i do it to make people think 💡
but i don't do it for lulz, i do it to make people think 💡
1
0
15
575
what is the most random 384-bit key? should it have exactly 192 ones and 192 zeros? no, that would be suspiciously symmetric
@ereliuer_eteer Treat the key as coin flipping. There is only one 1 of 384 bits. With a really strong Bernoulli prior like Beta(100,100), the new prior is Beta(483,101). Chance of it being fair-ish, P(0.45 < \theta < 0.55 | D), is 5.272\times10^{-46}, so astronomically small. (2/n)
3
0
15
1,784
use bayes, they say
okay
000
001
010
011
100
101
110
111
use bayes and tell me which one of these is less likely to be a result of a series of unbiased coin tosses
okay
000
001
010
011
100
101
110
111
use bayes and tell me which one of these is less likely to be a result of a series of unbiased coin tosses
it might sound counterintuitive but mathematically this combination has the same probability of being randomly generated as any other
10
0
37
10,224
Cleo retweeted
Amazing new project: github.com/google-deepmin…. Small Turing machines whose halting behavior encodes deep/interesting problems (by @MoritzFirsching).
0
3
15
1,331
Cleo retweeted
Fields Medalist Richard Borcherds on OpenAI proofs:
"i think what people are getting upset about is that they'e slowly realizing that they are dumb and somehow blaming this on AI, even though it's not really AI's fault"
finally, someone who gets it
"i think what people are getting upset about is that they'e slowly realizing that they are dumb and somehow blaming this on AI, even though it's not really AI's fault"
finally, someone who gets it
54
275
2,714
142,834
an idea: ubi in the form of discount for claude subscription
We’re committing a portion of Anthropic’s shares to the Anthropic Public Benefit Fund, a new wholly owned entity dedicated entirely to the public benefit.
It will start off with 5% of our shares. For every 50% increase in the company’s value over a set baseline, we can contribute up to an extra 2%, subject to our board’s discretion.
In total, this means that roughly 20% of Anthropic’s shares are committed to the public good. Our co-founders have already pledged to donate 80% of their equity, and around half our employees are donating a portion of their equity as part of a donation matching program we’ve run since our founding.
In the post below, we share more details about our new fund.
anthropic.com/news/public-be…
1
0
31
1,454
a little-known but fascinating conjecture about prime numbers
en.wikipedia.org/wiki/Gilbreath…
en.wikipedia.org/wiki/Gilbreath…
5
2
92
12,592
Cleo retweeted
BusyBeaver(230) is independent of ZFC! I have verified in Rocq that a certain 230-state Turing machine halts iff ZFC is inconsistent. This surpasses the non-formalized 243-state TM of @ereliuer_eteer and the formalized 254-state TM of @_Mira___Mira_.
11
65
532
28,659