All of Dacyn's Comments + Replies

Dacyn109

Basically both of these arguments will seem obvious if you fall into camp #2 here, and nonsensical if you fall into camp #1.

Dacyn12

Memento is easily one of the best movies about “rationality as practiced by the individual” ever made. [...] When the “map” is a panoply of literal paper notes and photographs, and the “territory” is further removed from one’s lived experience than usual… it behooves one to take rationality, bias, motivated cognition, unquestioned assumptions, and information pretty damn seriously!

Wasn't the main character's attempt at "rationality as practiced by the individual" kind of quixotic though? I didn't get the impression that the moral of the story was "you s... (read more)

2Nicholas / Heather Kross
I said "one of the best movies about", not "one of the best movies showing you how to".
Dacyn85

Let’s say my p(intelligent ancestor) is 0.1. Imagine I have a friend, Richard, who disagrees.

No wait, the order of these two things matters. Is P(intelligent ancestor|just my background information) = 0.1 or is P(intelligent ancestor|my background information + the fact that Richard disagrees) = 0.1? I agree that if the latter holds, conservation of expected evidence comes into play and gives the conclusion you assert. But the former doesn't imply the latter.

1Guive
I agree that the order matters, and I should have discussed that in the post, but I think the conclusion will hold either way. In the case where P(intelligent ancestor|just my background information) = 0.1, and I learn that Richard disagrees, the probability then goes above 0.1. But then when I learn that Richard's argument is bad it goes back down. And I think it should still go below 0.1, assuming you antecedently knew that there were some smart people who disagreed. You've learned that, for at least some smart intelligent ancestor believers, the arguments were worse than you expected.  
Answer by Dacyn84

What makes certain axioms “true” beyond mere consistency?

Axioms are only "true" or "false" relative to a model. In some cases the model is obvious, e.g. the intended model of Peano arithmetic is the natural numbers. The intended model of ZFC is a bit harder to get your head around. Usually it is taken to be defined as the union of the von Neumann hierarchy over all "ordinals", but this definition depends on taking the concept of an ordinal as pretheoretic rather than defined in the usual way as a well-founded totally ordered set.

Is there a meaningful

... (read more)
Dacyn32

I don't agree that I am making unwarranted assumptions; I think what you call "assumptions" are merely observations about the meanings of words. I agree that it is hard to program an AI to determine who the "he"s refer to, but I think as a matter of fact the meanings of those words don't allow for any other possible interpretation. It's just hard to explain to an AI what the meanings of words are. Anyway I'm not sure if it is productive to argue this any further as we seem to be repeating ourselves.

Dacyn32

No, because John could be speaking about himself administering the medication.

If it's about John administering the medication then you'd have to say "... he refused to let him".

It’s also possible to refuse to do something you’ve already acknowledged you should do, so the 3rd he could still be John regardless of who is being told what.

But the sentence did not claim John merely acknowledged that he should administer the medication, it claimed John was the originator of that statement. Is John supposed to be refusing his own requests?

2ymeskhout
The whole point of the sentence was to demonstrate how bad ambiguity can get with pronouns, and this exchange is demonstrating my point exactly. The issue might be that you're making some (very reasonable) assumptions without noticing it narrows the range of possible interpretations. The only unambiguous part of the sentence is "John told Mark", but every other he can be either John or Mark. Edit: my apologies for any rude tone, it was not intentional. All of us necessarily make reasonable assumptions to narrow ambiguity in our day to day conversations and it can be hard to completely jettison the habit.
Dacyn3-4

John told Mark that he should administer the medication immediately because he was in critical condition, but he refused.

Wait, who is in critical condition? Which one refused? Who’s supposed to be administering the meds? And administer to whom? Impossible to answer without additional context.

I don't think the sentence is actually as ambiguous as you're saying. The first and third "he"s both have to refer to Mark, because you can only refuse to do something after being told you should do it. Only the second "he" could be either John or Mark.

3ymeskhout
No, because John could be speaking about himself administering the medication. It's also possible to refuse to do something you've already acknowledged you should do, so the 3rd he could still be John regardless of who is being told what.
Dacyn40

Early discussion of AI risk often focused on debating the viability of various elaborate safety schemes humanity might someday devise—designing AI systems to be more like “tools” than “agents,” for example, or as purely question-answering oracles locked within some kryptonite-style box. These debates feel a bit quaint now, as AI companies race to release agentic models they barely understand directly onto the internet.

Why do you call current AI models "agentic"? It seems to me they are more like tool AI or oracle AI...

5Adam Scholl
I just meant there are many teams racing to build more agentic models. I agree current ones aren't very agentic, though whether that's because they're meaningfully more like "tools" or just still too stupid to do agency well or something else entirely, feels like an open question to me; I think our language here (like our understanding) remains confused and ill-defined. I do think current systems are very unlike oracles though, in that they have far more opportunity to exert influence than the prototypical imagined oracle design—e.g., most have I/O with ~any browser (or human) anywhere, people are actively experimenting with hooking them up to robotic effectors, etc.
Dacyn32

I am still seeing "succomb".

2lsusr
Thanks again. I fixed it for real this time.
Dacyn10

In the long scale a trillion is 10^18, not 10^24.

Dacyn10

I say "zero" when reciting phone numbers. Harder to miss that way.

1Andrew Burns
That's the wise thing to do, but people routinely use oh. Five-oh-six-three-four-oh-one. In fact, zero might sound overly formal to me depending on the context. If I am reading my credit card number, I would say zero.
Dacyn10

I think you want to define to be true if is true when we restrict to some neighbourhood such that is nonempty. Otherwise your later example doesn't make sense.

2Cleo Nardo
Edit: Wait, I see what you mean. Fixed definition. For Lewis, ∅?B=W for all B. In other words, the counterfactual proposition "were ϕ to occur then ψ would've occurred" is necessarily true if ϕ is necessarily false. For example, Lewis thinks "were 1+1=3, then Elizabeth I would've married" is true. This means that A∩N may be empty for all neighbourhoods N∈Nω, yet A?B is nonetheless true at w. Source: David Lewis (1973), Counterfactuals. Link: https://perso.uclouvain.be/peter.verdee/counterfactuals/lewis.pdf Elaborate?
Dacyn65

I noticed all the political ones were phrased to support the left-wing position.

Dacyn70

This doesn't completely explain the trick, though. In the step where you write f=(1-I)^{-1} 0, if you interpret I as an operator then you get f=0 as the result. To get f=Ce^x you need to have f=(1-I)^{-1} C in that step instead. You can get this by replacing \int f by If+C at the beginning.

4Robert_AIZI
Ah sorry, I skipped over that derivation! Here's how we'd approach this from first principals: to solve f=Df, we know we want to use the (1-x)=1+x+x^2+... trick, but now know that we need x=I instead of x=D. So that's why we want to switch to an integral equation, and we get f=Df If=IDf = f-f(0) where the final equality is the fundamental theorem of calculus. Then we rearrange: f-If=f(0) (1-I)f=f(0) and solve from there using the (1-I)=1+I+I^2+... trick! What's nice about this is it shows exactly how the initial condition of the DE shows up.
Dacyn21

If you find yourself thinking about the differences between geometric expected utility and expected utility in terms of utility functions, remind yourself that, for any utility function, one can choose* either* averaging method.

No, you can only use the geometric expected utility for nonnegative utility functions.

1MichaelStJules
If bounded below, you can just shift up to make it positive. But the geometric expected utility order is not preserved under shifts.
1A.H.
Thanks for pointing this out, I missed a word. I have added it now.
Dacyn10

It's obvious to us that the prompts are lying; how do you know it isn't also obvious to the AI? (To the degree it even makes sense to talk about the AI having "revealed preferences")

Dacyn106

Calvinists believe in predestination, not Protestants in general.

Dacyn43

Wouldn't that mean every sub-faction recursively gets a veto? Or do the sub-faction vetos only allow the sub-faction to veto the faction veto, rather than the original legislation? The former seems unwieldy, while the latter seems to contradict the original purpose of DVF...

1Joseph Miller
The subfaction veto only applies to faction level policy. The faction veto is decided by pure democracy within the faction. I would guess in most scenarios most subfactions would agree when to use the faction veto. Eg. all the Southern states didn't want to end slavery.
Dacyn10

(But then: aren’t there zillions of Boltzmann brains with these memories of coherence, who are making this sort of move too?)

According to standard cosmology, there are also zillions of actually coherent copies of you, and the ratio is heavily tilted towards the actually coherent copies under any reasonable way of measuring. So I don't think this is a good objection.

Dacyn10

“Only food that can be easily digested will provide calories”

That statement would seem to also be obviously wrong. Plenty of things are ‘easily digested’ in any reasonable meaning of that phrase, while providing ~0 calories.

I think you've interpreted this backwards; the claim isn't that "easily digested" implies "provides calories", but rather that "provides calories" implies "easily digested".

2gwern
Well, debates about what modal operators are meant by 'only' aside, I am doubtful that claim is true either! First, as a parallel consider grass again: to digest grass, ruminants need an extremely long intestinal system which takes multiple passes (including throw it up to the mouth to chew it again, for hours on end, chewing their cud again and again) and requires tons of microbes to digest it over multiple days; again, under any ordinary understanding of the phrase 'easily digested', it is not easy for cows to digest grass. Yet they still get all the calories they need to live on from it. So, for cows, grass 'provides calories' and yet is not 'easily digested'. This is also true for humans: eating plants and raw uncooked foods 'provide calories', but are not 'easily digested'; in fact, they provide much less net calories than they should because so many calories go right back into the digestive process.* (And this is one of the major theories for the importance of fire & cooking in human evolution: 'the expensive gut tissue' hypothesis.) You could also point to things like 'poisonous berries': you eat them and enjoy calories as their simple carbohydrates easily digest... until you then lose a bunch of calories by being sick and sh−ting yourself all day long. Easily digested, without a doubt but did they provide calories? They did - but only for the first few hours. So, this brings out that when you talk about 'easily digested things' which 'provides calories', you are implicitly including the caloric costs of digestion & side-effects and it's really net calories you are talking about. Which will also be context-specific (eg. presumably there are wild animals like birds who will be immune to the berry poison and are the intended consumers, and for them the berries deliver full caloric value). * see also: the malnourishment of 'raw foodists', which manifests in symptoms like menstruation stopping.
Dacyn80

In constructivist logic, proof by contradiction must construct an example of the mathematical object which contradicts the negated theorem.

This isn't true. In constructivist logic, if you are trying to disprove a statement of the form "for all x, P(x)", you do not actually have to find an x such that P(x) is false -- it is enough to assume that P(x) holds for various values of x and then derive a contradiction. By contrast, if you are trying to prove a statement of the form "there exists x such that P(x) holds", then you do actually need to construct an example of x such that P(x) holds (in constructivist logic at least).

4depressurize
The way I think of it, is that constructivist logic allows "proof of negation" via contradiction which is often conflated with "proof by contradiction". So if you want to prove ¬P, it's enough to assume P and then derive a contradiction.  And if you want to prove ¬¬P,  it's enough to assume ¬P and then derive a contradiction. But if you want to prove P, it's not enough to assume ¬P and then derive a contradiction. This makes sense I think - if you assume ¬P and then derive a contradiction, you get ¬¬P,  but in constructivist logic there's no way to go directly from ¬¬P to P. Proof of negation (allowed): Prove ¬P by assuming P and deriving a contradiction Proof by contradiction (not allowed): Prove P by assuming ¬P and deriving a contradiction
Dacyn10

Just a technical point, but it is not true that most of the probability mass of a hypothesis has to come from "the shortest claw". You can have lots of longer claws which together have more probability mass than a shorter one. This is relevant to situations like quantum mechanics, where the claw first needs to extract you from an individual universe of the multiverse, and that costs a lot of bits (more than just describing your full sensory data would cost), but from an epistemological point of view there are many possible such universes that you might be a part of.

Dacyn10

As I understood it, the whole point is that the buyer is proposing C as an alternative to A and B. Otherwise, there is no advantage to him downplaying how much he prefers A to B / pretending to prefer B to A.

Dacyn10

Hmm, the fact that C and D are even on the table makes it seem less collaborative to me, even if you are only explicitly comparing A and B. But I guess it is kind of subjective.

1jchan
It's a question of whether drawing a boundary on the "aligned vs. unaligned" continuum produces an empirically-valid category; and to this end, I think we need to restrict the scope to the issues actually being discussed by the parties, or else every case will land on the "unaligned" side. Here, both parties agree on where they stand vis-a-vis C and D, and so would be "Antagonistic" in any discussion of those options, but since nobody is proposing them, the conversation they actually have shouldn't be characterized as such.
Dacyn10

It seems weird to me to call a buyer and seller's values aligned just because they both prefer outcome A to outcome B, when the buyer prefers C > A > B > D and the seller prefers D > A > B > C, which are almost exactly misaligned. (Here A = sell at current price, B = don't sell, C = sell at lower price, D = sell at higher price.)

1Stuart Johnson
I think the important value here is not the assets changing hands as part of the exchange, but rather the value each party stands to gain from the exchange. Both parties are aligned that shaking hands on the current terms is acceptable to them, but they will both lie about that fact if they think it helps them move towards C or D.  Or to put it another way, in your frame I don't think any kind of collaboration can ever be in anyone's interests unless you are aligned in Every Single Thing. If I save a drowning person, in a mercenary way it is preferable to them that I not only save them but also give them my wallet. Therefore my saving them was not a product of aligned interests (desire to not drown + desire to help others) since the poor fellow must now continue to pay off his credit card debt when his preference is to not do that. For me, B > A > D > C, and for the drowning man,  A > B > C > D (Here A = rescue + give wallet, B = rescue, no wallet, C = no rescue, throw wallet into water, D = walk away) What matters in the drowning relationship (and the reason for our alignment) is B > C. Whether or not I give him my wallet is an independent variable from whether I save him and the resulting alignment should be considered separately. In your example, I'm focusing on the alignment of A and B. Both parties will be dishonest about their views on A and B if they think it gets them closer to alignment on C and D. That's the insincerity.
Dacyn10

Isn't the fact that the buyer wants a lower price proof that the seller and buyer's values aren't aligned?

1Stuart Johnson
In almost all cases, the buyer will grossly exaggerate the degree to which values are not aligned in the hopes of driving the seller down in price. In most cases, the buyer has voluntarily engaged the seller (or even if they haven't, if they consider the deal worth negotiating then there must be some alignment of values).  Even if I think the price is already acceptable to me, I will still haggle insincerely because of the prospect of an even better deal.
Dacyn22

You're right that "Experiencing is intrinsically valuable to humans". But why does this mean humans are irrational? It just means that experience is a terminal value. But any set of terminal values is consistent with rationality.

1martinkunev
Maybe "irrational" is not the right word here. The point I'm trying to make is that human preferences are not over world states. When discussing preference rationality, arguments often consider only preferences over states of the world, while ignoring transitions between those states. For example, a person in San Francisco may drive to San Jose, then to Oakland and then back to San Francisco simply because they enjoy moving around. Cyclic transition between states is not necessarily something that needs fixing.
Dacyn31

Of course, from a pedagogical point of view it may be hard to explain why the "empty function" is actually a function.

Dacyn30

When you multiply two prime numbers, the product will have at least two distinct prime factors: the two prime numbers being multiplied.

Technically, it is not true that the prime numbers being multiplied need to be distinct. For example, 2*2=4 is the product of two prime numbers, but it is not the product of two distinct prime numbers.

As a result, it is impossible to determine the sum of the largest and second largest prime numbers, since neither of these can be definitively identified.

This seems wrong: "neither can be definitively identified" makes ... (read more)

4VipulNaik
Thanks for reviewing and catching these subtle issues! Good point, I've marked this as an error. My prompt about gcd did specify distinctness but the prompt about product did not, so this is indeed an error. I passed on this one as being too minor to mark. Good point; I missed reading this sentence originally. I've marked this one as well.
Dacyn10

OK, that's fair, I should have written down the precise formula rather than an approximation. My point though is that your statement

the expected value of X happening can be high when it happens a little (because you probably get the good effects and not the bad effects Y)

is wrong because a low probability of large bad effects can swamp a high probability of small good effects in expected value calculations.

2DanielFilan
A low probability of large bad effects can swamp a high probability of small good effects, but it doesn't have to, so you can have the high probability of small good effects dominate.
Dacyn1-2

Yeah, but the expected value would still be .

2DanielFilan
No. The probability of K balls all being the good balls (assuming you're drawing with replacement) is ((N-1)/N)^K. So the expected value is ((N-1)/N)^K x (KxA) - (1 - ((N-1)/N)^K) x B
Dacyn10

I don't see why you say Sequential Proportional Approval Voting gives little incentive for strategic voting. If I am confident a candidate I support is going to be elected in the first round, it's in my interest not to vote for them so that my votes for other candidates I support will count for more. Of course, if a lot of people think like this then a popular candidate could actually lose, so there is a bit of a brinksmanship dynamic going on here. I don't think that is a good thing.

3Marcus Ogren
You have to be careful with this argument because it's valid for any candidate-based proportional voting method. All such voting methods rely on the influence of voters who strongly support candidates who get elected being reduced with regard to other candidates, so all of them have such an incentive. (It takes different forms in different voting methods; in STV the incentive isn't to forgo ranking such a candidate altogether, it's to rank such a candidate second or third.) This does not mean the incentive for free-riding is equally strong under all candidate-based proportional voting methods, however, and I do think that strategy is more important under SPAV than under some forms of STV.
Dacyn10

The definition of a derivative seems wrong. For example, suppose that for rational but for irrational . Then is not differentiable anywhere, but according to your definition it would have a derivative of 0 everywhere (since could be an infinitesimal consisting of a sequence of only rational numbers).

2Yudhister Kumar
Have updated the definition of the derivative to specify the differences between f over the hyperreals and f over the reals. I think the natural way to extend your f to the hyperreals is for it to take values in an infinitesimal neighborhood surrounding rationals to 0 and all other values to 1. Using this, the derivative is in fact undefined, as st(0/Δx)=0/st(Δx)=0/0.
Dacyn10

But if they are linearly independent, then they evolve independently, which means that any one of them, alone, could have been the whole thing—so why would we need to postulate the other worlds? And anyway, aren’t the worlds supposed to be interacting?

Can't this be answered by an appeal to the fact that the initial state of the universe is supposed to be low-entropy? The wavefunction corresponding to one of the worlds, run back in time to the start of the universe, would have higher entropy than the wavefunction corresponding to all of them together, so it's not as good a candidate for the starting wavefunction of the universe.

Dacyn20

No, the whole premise of the face-reading scenario is that the agent can tell that his face is being read, and that's why he pays the money. If the agent can't tell whether his face is being read, then his correct action (under FDT) is to pay the money if and only if (probability of being read) times (utility of returning to civilization) is greater than (utility of the money). Now, if this condition holds but in fact the driver can't read faces, then FDT does pay the $50, but this is just because it got unlucky, and we shouldn't hold that against it.

Dacyn42

In your new dilemma, FDT does not say to pay the $50. It only says to pay when the driver's decision of whether or not to take you to the city depends on what you are planning to do when you get to the city. Which isn't true in your setup, since you assume the driver can't read faces.

1Augs SMSHacks
The agent in this scenario doesn't necessarily know if the driver can read faces or not, in the original problem the agent isn't aware of this information. Surely if FDT advises you pay him on arrival in the face reading scenario, you would do the same in the non-face reading scenario since the agent can't tell them apart.
Dacyn1212

a random letter contains about 7.8 (bits of information)

This is wrong, a random letter contains log(26)/log(2) = 4.7 bits of information.

1abramdemski
Whoops! Thanks.
Dacyn10

This only works if Omega is willing to simulate the Yankees game for you.

Dacyn41

I have tinnitus every time I think about the question of whether I have tinnitus. So do I have tinnitus all the time, or only the times when I notice?

Dacyn30

I was confused at first what you meant by "1 is true" because when you copied the post from your blog you didn't copy the numbering of the claims. You should probably fix that.

Dacyn31

The number 99 isn’t unique—this works with any payoff between 30 and 100.

Actually, it only works with payoffs below 99.3 -- this is the payoff you get by setting the dial to 30 every round while everyone else sets their dials to 100, so any Nash equilibrium must beat that. This was mentioned in jessicata's original post.

Incidentally, this feature prevents the example from being a subgame perfect Nash equilibrium -- once someone defects by setting the dial to 30, there's no incentive to "punish" them for it, and any attempt to create such an incentive via a "punish non-punishers" rule would run into the trouble that punishment is only effective up to the 99.3 limit.

Dacyn10

It's part of the "frontpage comment guidelines" that show up every time you make a comment. They don't appear on GreaterWrong though, which is why I guess you can't see them...

Dacyn10

I explained the problem with the votes-per-dollar formula in my first post. 45% of the vote / $1 >> 55% of the vote / $2, so it is not worth it for a candidate to spend money even if they can buy 10% of the vote for $1 (which is absurdly unrealistically high).

When I said maybe a formula would help, I meant a formula to explain what you mean by "coefficient" or "effective exchange rate". The formula "votes / dollars spent" doesn't have a coefficient in it.

If one candidate gets 200 votes and spends 200 dollars, and candidate 2 gets 201 votes and spen

... (read more)
1Adam Golding
"it is not worth it for a candidate to spend money even if they can buy 10% of the vote for $1 (which is absurdly unrealistically high)." So what is a realistic price / 'exchange rate' for this example, in your opinion?   I provided a coefficient of '1' spelled out in the line below that, it could be '10' or '100', etc. "Sure, and my proposal of Votes / (10X + Y) would imply that the first candidate wins." Which invariant(s) would you construe this as maintaining?  Why not just add a constant coefficient?  This is more efficient to compute, and the average price is already too high, that's 'half the point'.
Dacyn10

I don't think the data dependency is a serious problem, all we need is a very loose estimate. I don't know what you mean by a "spending barrier" or by "effective exchange rate", and I still don't know what coefficient you are talking about. Maybe it would help if you wrote down some formulas to explain what you mean.

1Adam Golding
"votes-per-dollar" IS a formula -- aka v/d -- 'per' means division -- spelling out the coefficient we have: 1*v/d where 'undefined' is ranked last and infinity is not a return value OR 1*v/(1+d) where 1/0 approached from the right is +inf (there are no negative votes  -- if dollars are negative eg a campaign turns a profit we could take abs(1+d) or abs(d) as the denominator) v = total votes for the candidate d = total dollars spent by the candidate But here's a basic unit test, riddle me this: If one candidate gets 200 votes and spends 200 dollars, and candidate 2 gets 201 votes and spends two MILLION dollars, who has the strongest mandate, in the sense that the representative actually represents the will of the people when wealth differences are ignored?
Dacyn10

I don't understand what you mean; multiplying the numerator by a coefficient wouldn't change the analysis. I think if you wanted to have a formula that was somewhat sensitive to campaign spending but didn't rule out campaign spending completely as a strategy, Votes/(10X+Y) might work, where Y is the amount spent of campaign spending, and X is an estimate of average campaign spending. (The factor of 10 is because campaign spending just isn't that large a factor to how many votes you get in absolute terms; it's easy to get maybe 45% of the vote with no campaign spending at all, just by having (D) or (R) in front of your name.)

1Adam Golding
This counterproposal has a data dependency where we need to know averages from the past, and also will still present a spending barrier for dirt-poor candidates if the average happens to be large (it is). What I meant in response to your original comment is that whether it's 'worth it' depends on the current 'effective exchange rate' between votes and dollars, which is represented by a coefficient of '1' in this first approximation.  There should presumably be an update rule for 'learning' the 'correct' coefficient....
Dacyn20

The result of this will be that no one will spend more than the $1 minimum. It's just not worth it. So your proposal is basically equivalent to illegalizing campaign spending.

1Adam Golding
what coefficient in the numerator would change your conclusion?
Dacyn64

I wonder whether this one is true (and can be easily proved): For a normal form game G and actions ai for a player i, removing a set of actions a−i from the game yields a game G− in which the Nash equilibria are worse on average for i (or alternatively the pareto-best/pareto-worst Nash equilibrium is worse for G− than for G).

It's false: consider the normal form game

(0,0) (2,1)

(1,1) (3,0)

For the first player the first option is dominated by the second, but once the second player knows the first player is going to choose the second option, he's moti... (read more)

Dacyn43

Not eating meat is not a Pascal's mugging because there is a solid theoretical argument for why the expected value is positive even if the payoff distribution is somewhat unbalanced: if a large number of people decide not to eat meat, then this will necessarily have the effect of shifting production, for supply to meet demand. Since you have no way of knowing where you are in that large ensemble, the expected value of you not eating meat is equal to the size of the effect divided by the number of people in the ensemble, which is presumably what we would ex... (read more)

Dacyn10

A proof you don’t understand does not obligate you to believe anything; it is Bayesian evidence like anything else. If an alien sends a 1GB Coq file Riemann.v, running it on your computer does not obligate you to believe that the Riemann hypothesis is true. If you’re ever in that situation, do not let anyone tell you that Coq is so awesome that you don’t roll to disbelieve. 1GB of plaintext is too much, you’ll get exhausted before you understand anything. Do not ask the LLM to summarize the proof.

I'm not sure what you are trying to say here. Even with 1... (read more)

1Quinn
I think a coq bug or the type of mistakes that are easy to make in formalization are more likely than a transistor failure or a bad bit flip bubbling up through the stack, but still not what I'm talking about. In the background, I'm thinking a little about this terry tao post, about how the process of grokking the proof (and being graceful with typos, knowing which typos are bad and which are harmless, and so on) is where the state of the art mathematics lies, not in the proof itself. I was discussing your comment with a friend, who suggested what I'm calling factored cognition parallel auditing (FCPA): she asked why don't we just divide the 1e6 lines of coq into 1000-line segments and send it out to 1000 experts each of whom make sense of their segment? The realities would be a little messier than linearly stitching together segments, but this basic setup (or something that emphasizes recursion, like a binary search flavored version) would I think buy us roughly 2-3x the assurance that RH true over just blindly trusting the type theory / laptop to execute Riemann.v in the coq session. In the current comment, let's assume a background of russell-like "enfeeblement" or christiano-like "losing control of the world/future in a slow burn", filtering out the more yudkowsky-like threatmodels. Not to completely discount malicious injections in Riemann.v, but they don't seem productive to emphasize. I will invoke the vague notions of "theorem intricacy" and "proof length", but it should be possible to not read this footnote[1] and still follow along with the goals of the current comment. This isn't really about RH, RH isn't necessarily important, etc. I was actually alluding to / vaguely criticizing a few different ideas at once in the paragraph you quoted. 1. The proof assistants or applied type theory technologies will help agent foundations researchers progress and/or teach. I'm bearish on this largely because I think agent foundations researchers care more about t
Load More