Just how bad of an idea is it for someone who knows programming and wants to learn math to try to work through a mathematics textbook with proof exercises, say Rudin's *Principles of Mathematical Analysis*, by learning a formal proof system like Coq and using that to try to do the proof exercises?

I'm figuring, hey, no need to guess whether whatever I come up with is valid or not. Once I get it right, the proof assistant will confirm it's good. However, I have no idea how much work it'll be to get even much simpler proofs that what are expected of the textbook reader right, how much work it'll be to formalize the textbook proofs even if you do know what you're doing and whether there are areas of mathematics where you need an inordinate amount of extra work to get machine-checkable formal proofs going to begin with.

I have tried exactly this with basic topology, and it took me bloody ages to get anywhere despite considerable experience with coq. It was a fun and interesting exercise in both the foundations of the topic I was studying and coq, but it was by no means the most efficient way to learn the subject matter.

Hm... yes, I can't say your formula is obviously right, but mine is obviously inconsistent. I guess I owe Nick ninety-seven cents.

My take on it:

You judge an odds ratio of 15:85 for the money having been yours versus it having been Nick's, which presumably decomposes into a maximum entropy prior (1:1) multiplied by whatever evidence you have for believing it's not yours (15:85). Similarly, Nick has a 80:20 odds ratio that decomposes into the same 1:1 prior plus 80:20 evidence.

In that case, the combined estimate would be the combination of both odds ratios applied to the shared prior, yielding a 1:1 * 15:85 * 80:20 = 12:17 ratio for the money being yours versus it being Nicks. Thus, you deserve 12/29 of it, and Nick deserves the remaining 17/29.

I'd expect Voldy to know about it and request clarification

Not necessarily. Parseltongue, if I understand it correctly, forces the speaker to *tell the truth as he/she understands it* (while bypassing Occlumency). If *Harry* knows about material implication (which he almost certainly does), *he* can utilize it in such a manner, but it's unlikely that *Voldemort* has ever encountered something similar. This isn't your standard clever wordplay that anyone smart can think of, after all--it's formal logic, which is decidedly Muggle.

So it's nonstandard clever wordplay. Voldemort will still anticipate a nontrivial probability of Harry managing undetected clever wordplay. Which means it only has a real chance of working when threatening something that Voldemort can't test immediately.

After 5 minutes of thinking about it, the only thing I could come up with concerns:

"HE IS HERE. THE ONE WHO WILL TEAR APART THE VERY STARS IN HEAVEN. HE IS HERE. HE IS THE END OF THE WORLD."

Bellatrix and Sirius are stars, and also Death Eaters. Voldemort has already torn apart Bellatrix to use the Dark Mark, and Harry can tear apart Sirius with the Partial Transfiguration trick people are talking about. How do we know Sirius is present? Because there is a Death Eater named "Mr Grim" who is stated to have known the Potters.

Hang on, isn't Sirius in Azkaban?

"I'm not serious, I'm not serious, I'm not serious..."

The "he" refers to both Tom Riddles, as they are branches of the same person.

Troubles with this suggestion:

The "HE IS THE END OF THE WORLD" part remains unresolved.

Narratively unsatisfying.

I don't think this is likely, if only because of the unsatisfyingness. However:

And the messages would come out in riddles, and only someone who heard the prophecy in the seer's original voice would hear all the meaning that was in the riddle. There was no possible way that Millicent could just give out a prophecy any time she wanted, about school bullies, and then remember it, and if she had it would've come out as 'the skeleton is the key' and not 'Susan Bones has to be there'. (Ch.77)

Some foreshadowing on the idea of ominous-sounding prophecy terms actually referring to people's names.

Beneath the moonlight glints a tiny fragment of silver, a fraction of a line... (black robes, falling) ...blood spills out in litres, and someone screams a word.

"blood spills out in litres" meshes well with "TEAR APART".

MIRI Mission/MIRI Effectiveness .395 (1331)

This result sets off my halo effect alarm.

Seconded. P versus NP is the most important piece of the basic math of computer science, and a basic notion of algorithms is a bonus. The related broader theory which nonetheless still counts as basic math is algorithmic complexity and the notion of computability.

What's the deal with spells and age? If Harry is really so far ahead of his class and can already cast spells nobody else can, why is it *just now* that he can cast "second-year" spells effortlessly?

Canon or not, this reminds me too much of the public school system of a certain country where kids are verboten to use words "they shouldn't know yet".

I've always modeled it as a physiological "mana capacity" aspect akin to muscle mass -- something that grows both naturally as a developing body matures, and as a result of exercise.

View more: Next

My interpretation of this thesis immediately remind me of Eliezer's post on locality and compactness of specifications, among others.

Under this framework, my analysis is that triangle-ness has a specification that is both compact and local; whereas L-opening-ness has a specification that is compact and nonlocal ("opens L"), and a specification that is local but noncompact (a full specification of what shapes it is and is not allowed to have), but no specification that is both local and compact. In other words, there is a

shortspecification which refers to something external (L) and alonglookup-table specification that talks only about the key.I think this is the sensible way of caching out your notion of intrinsicness. (Intrinsicity? Intrinsicitude?)

In this interpretation, I don't think human morality should be judged as non-intrinsic. The shortest local specification of our values is not particularly compact; but neither can you resort to a nonlocal specification to find something more compact. "Whatever makes me happy" is

notthe sum of my morality, nor do I think you will find a simple specification along those lines that refers to the inner workings of humans. In other words, the specification of human morality is not something you can easily shorten by referring to humans.