Posts

Comments

Comment by Risto_Saarelma on [deleted post] 2017-09-03T08:33:24.892Z

This isn't working for me as pumping the intuition you seem to want it to. I think life is worth living and I'd just cut to the chase and pick 1 because option 2 doesn't make sense as a way to get more life. Pattern theory of identity, life is a process, not a weighted lump of time-space-matter-stuff where you can just say "let's double the helping" like this. If you run the exact same process twice, that doesn't get you any new patterns and new life compared to just running it once.

Or if the idea is that I'd be aware of having gotten a second run, the part about the exact same decisions and experiences seems to make this amount to spending a few decades watching a boring home video with nothing you-on-second-trip can do about it and constantly aware that you'll be annihilated at the end. I guess the "maybe the horse will learn to sing" thinking would make sense here, but that's just fighting the hypothetical that the thought experiment will unfold exactly as described.

Comment by Risto_Saarelma on Ten small life improvements · 2017-08-30T05:46:40.796Z · LW · GW

And for people on the Vim side, there's VimOutliner for doing workflowy-like outlines, also with a time-tracking component.

Comment by Risto_Saarelma on Stupid Questions December 2016 · 2016-12-22T05:29:34.080Z · LW · GW

Cal Newport on "Write Every Day". If it's not your main job, you're going to end up having no write days, and if you're committed to a hard schedule a missed day is going to translate into "welp, couldn't make the cut then, better quit for good".

Comment by Risto_Saarelma on Open Thread, Aug. 22 - 28, 2016 · 2016-08-26T05:18:19.364Z · LW · GW

On Moldbug from 2012.

Comment by Risto_Saarelma on February 2016 Media Thread · 2016-02-04T18:10:52.917Z · LW · GW

Yes, The Mind Illuminated is basically the same ten-step model as the one in that article, but expanded to book length and with lots of extra practice advice and theory of mental models.

Comment by Risto_Saarelma on February 2016 Media Thread · 2016-02-02T04:59:27.911Z · LW · GW

The Mind Illuminated by John Yates is my new favorite meditation instruction book. Has lots of modern neuroscience grounding, completely secular, and presents a very detailed step-by-step instruction on going from not having a daily meditation habit going to attaining very deep concentration states.

Comment by Risto_Saarelma on [Link] AlphaGo: Mastering the ancient game of Go with Machine Learning · 2016-01-31T08:41:56.299Z · LW · GW

One problem is that the community has few people actually engaged enough with cutting edge AI / machine learning / whatever-the-respectable-people-call-it-this-decade research to have opinions that are grounded in where the actual research is right now. So a lot of the discussion is going to consist of people either staying quiet or giving uninformed opinions to keep the conversation going. And what incentive structures there are here mostly work for a social club, so there aren't really that many checks and balances that keep things from drifting further away from being grounded in actual reality instead of the local social reality.

Ilya actually is working with cutting edge machine learning, so I pay attention to his expressions of frustration and appreciate that he persists in hanging out here.

Comment by Risto_Saarelma on [deleted post] 2016-01-30T08:51:17.720Z

Congratulations on getting a "ban any new user posting the sort of stuff Eugine would post" moderation norm on the way I guess.

Comment by Risto_Saarelma on Open thread, Jan. 25 - Jan. 31, 2016 · 2016-01-29T19:46:11.829Z · LW · GW

This sounds like someone who's salient feature is math anxiety from high school asking how to be a research director at CERN. It's not just that the salient feature seems at odds with the task, it's that the task isn't exactly something you just walk into, while you sound like you're talking about helping someone overcome a social phobia by taking a part-time job at supermarket checkout. Is your friend someone who wins International Math Olympiads?

Comment by Risto_Saarelma on LessWrong 2.0 · 2016-01-10T09:45:55.115Z · LW · GW

Maybe someday someone clever will figure out how to disseminate that knowledge, but it simply isn't there yet.

Based on Razib Khan's blog posts, many cutting edge researchers seem to be pretty active on Twitter where they can talk about their own stuff and keep up on what their colleagues are up to. Grad students on social media will probably respond to someone asking about their subfield if it looks like they know their basics and may be up to something interesting.

The tiny bandwidth is of course a problem. "Professor Z has probably proven math lemma A" fits in a tweet, instruction on lab work rituals not so much.

Clever people who don't want to pay for plane tickets and tuition might be pretty resourceful though, once they figure out they want to talk with each other to learn what they need to know.

Comment by Risto_Saarelma on LessWrong 2.0 · 2016-01-10T05:32:06.770Z · LW · GW

I am quite certain this is very unlikely to become any type of trend (it is certainly possible for outsiders to be great, Ramanujan was an outsider after all).

Not in the present circumstances, no. The interesting thing is if it would strike a match with the current disaffection with academia (perceptions of must-have-bachelor's-for-any-kind-of-job student loan rackets and stressed-out researchers who spend most of their energy gaming administrative systems and grinding out cookie-cutter research tailored to fit standardized bureaucratic metrics for acceptable tenure-track career path progress), cause more young people who think they are talented and exceptional to drop out, and what they will do once they have and if that trend might continue far enough to change the wider circumstances around academia.

Comment by Risto_Saarelma on LessWrong 2.0 · 2016-01-09T08:57:44.110Z · LW · GW

Yeah, I am sure enough about this not happening that I am willing to place bets. There is an enormous amount of intangibles Coursera can't give you (I agree it can be useful for a certain type of person for certain types of aims).

Agree that being inside academia is probably a lot bigger deal than people outside it really appreciate. We're about to see the first generation that grew up with a really ubiquitous internet come to grad school age though. Currently in addition to the assumption that generally clever people will want to go to university, we've treated it as obvious that the Nobel prize winning clever people will have an academic background. Which has been pretty much mandatory, since that used to be the only way you got to talk with other academicians and to access academic publications.

What I'm interested in now is whether in the next couple decades we're going to see a Grigori Perelman or Shinichi Mochizuki style extreme outlier produce some result that ends up widely acknowledged to be an equally big deal as what Perelman did, without ever having seen the inside of an university. You can read pretty much any textbook or article you want over an internet connection now, and it's probably not impossible to get professional mathematicians talking with you even when they have no idea who you are if it's evident from the start that you have some idea what their research is about. And an extreme outlier might be clever enough to figure things on their own, obsessive enough to keep working on them on their own for years, and somewhat eccentric so that they take a dim view on academia and decline to play along out of principle.

It'd basically be a fluke statistically, but it would put a brand new spin on the narrative about academia. Academia wouldn't be the obvious one source of higher learning anymore, it'd be the place where you go when you're pretty smart but not quite good and original enough to go it alone.

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-08T20:29:15.404Z · LW · GW

Yeah, for some reason I'm not inclined to give very much weight to an event that can't be detected by outside observers at all and which my past, present or future selves can't subjectively observe being about to happen, happening right now or having happened.

You seem to be hung up on either memories or observations being the key to decoding the subjective self. I think that is your error.

This sounds like a thing people who want to explain away subjective consciousness completely are saying. I'm attacking the notion that the annoying mysterious part in subjective consciousness with the qualia and stuff includes a privileged relation from the present moment of consciousness to a specific future moment of consciousness, not the one that there's subjective consciousness stuff to begin with that isn't easy to reduce to just objective memories and observations.

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-08T06:02:22.765Z · LW · GW

There is some Buddhist connection, yes. The moments of experience thing is a thing in some meditation styles, and advanced meditators are actually describing something like subjective experience starting to feel like an on/off sequence instead of a continuous flux. Haven't gone really deep into what either the Buddhist metaphysics or the meditation phenomenology says. Neuroscience also has some discrete consciousness steps stuff, but I likewise haven't gone very deep into that. Anyway,

I'm with them so far. Here's where I get off): All sentient beings are points of naked awareness, by definition they are identical (naked, passive), therefore they are the same, Therefore even this self does not matter, therefore thou shall not value the self more than others. At all. On any level. All of which can lead you to bricking yourself up in a cave being the correct course of action.

This is still up for grabs. Given the whole thing about memories being what makes you you, consciousness itself is nice but it's not all that. It can still be your tribe against the world, your family against your tribe, your siblings against your family and you and your army of upload copies against your siblings and their armies of upload copies. So I'm basically thinking about this from a kin altruism and a general having people more like you closer in your circle of concern than people less like you thing. Upload copies are basically way, way closer kin than any actual kin.

So am I a pattern theorist? Not quite sure. It seems to resolve lots of paradoxes with the upload thought experiments, and I have no idea about a way to prove it wrong. (Would like to find one though, it seems sorta simplistic and we definitely still don't understand consciousness to my satisfaction.) But like I said, if I sit down on an upload couch, I fully expect to get up from an upload couch, not suddenly be staring at a HUD saying "IN SIMULATION", even though pattern theory seems to say that I should expect each outcome with 50 % probability. There will be someone who does wake up in the simulation with my memories in the thought experiment, no matter which interpretation, so I imagine those versions will start expecting to shift viewpoints while they do further upload scans, while the version of me who always wakes up on the upload coach (by the coin-toss tournament logic, there will be a me who never experiences waking up in a simulation, and one who always does) will continue to not expect much. I think uploads are a good idea more because of the kin selection like reasons above rather than because I'm convinced it's a ticket to personal immortality.

I wouldn't give a damn about aliens taking my body and brain apart every time I sleep as long as they put it back together perfectly again though, so if that makes me a pattern theorist then yes.

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-08T05:31:22.432Z · LW · GW

The strange part that might give your intuition a bit of a shake is that it's not entirely clear how you tell the difference as an inside observer either. The thought experiment wasn't "we're going to start doing this tomorrow night unless you acquiesce", it's "we've been doing this the whole time", and everybody had been living their life exactly as before until told about it. What should you now think of your memories of every previous day and going to sleep each night?

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-07T18:47:00.623Z · LW · GW

My expounding of the pattern identity theory elsewhere in the comments is probably a textbook example of what Scott Aaronson calls bullet-swallowing, so just to balance things out I'm going to link to Aaronson's paper Ghost in the Quantum Turing Machine that sketches a very different attack on standard naive patternism. (Previous LW discussion here)

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-07T18:26:58.812Z · LW · GW

If pressed, right now I'm leaning towards the matter-based argument, that if consciousness is not magical then it is tied to specific sets of matter. And that a set of matter can not exist in multiple locations. Therefore a single consciousness can not exist in multiple locations. The consciousness A that I am now is in matter A.

So, there are two things we need to track here, and you're not really making a distinction between them. There are individual moments of consciousness, which, yes, probably need to be on a physical substrate that exists in the single location. This is me saying that I'm this moment of conscious experience right now, which manifests in my physical brain. Everybody can be in agreement about this one.

Then there is the continuity of consciousness from moment to moment, which is where the problems show up. This is me saying that I'm the moment of conscious experience in my brain right now, and I'm also going to be the next moment of conscious experience in my brain.

The problems start when you want to say that the moment of consciousness in your brain now and the moment of consciousness in your brain a second in the future are both "your consciousness" and the moment of consciousness in your brain now and the moment of consciousness in your perfect upload a second in the future are not. There is no actual "consciousness" that refers to things other than the single moments for the patternist. There is momentary consciousness now, with your memories, then there is momentary consciousness later, with your slightly evolved memories. And on and on. Once you've gone past the single eyeblink of consciousness, you're already gone, and a new you might show up once, never, or many times in the future. There's nothing but the memories that stay in your brain during the gap laying the claim for the you-ness of the next moment of consciousness about to show up in a hundred or so milliseconds.

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-07T07:18:04.902Z · LW · GW

You're still mostly just arguing for your personal intuition for the continuity theory though. People have been doing that pretty much as long as we've had fiction about uploads or destructive teleportation, with not much progress to the arguments. How would you convince someone sympathetic to the pattern theory that the pattern theory isn't viable?

FWIW, after some earlier discussions about this, I've been meaning to look into Husserl's phenomenology to see if there are some more interesting arguments to be found there. That stuff gets pretty weird and tricky fast though, and might be a dead end anyway.

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-07T06:40:20.115Z · LW · GW

I'm guessing a part of the point is that nobody had noticed anything (and indeed still can't, at least in any way they could report back) until the arrangement was pointed out, which highlights that there are bits in the standard notion of personal identity that get a bit tricky once you try to get more robust than just going by intuition on them. How do you tell you die when a matrix lord disintegrates you and then puts together an identical copy? How do you tell you don't die when you go under general anesthesia for brain surgery and then wake up?

Comment by Risto_Saarelma on Your transhuman copy is of questionable value to your meat self. · 2016-01-06T21:20:40.346Z · LW · GW

I see the pattern identity theory, where uploads make sense, as one that takes it as a starting point that you have an unambiguous past but no unambiguous future. You have moments of consciousness where you remember your past, which gives you identity, and lets you associate your past moments of consciousness to your current one. But there's no way, objective or subjective, to associate your present moment of consciousness to a specific future moment of consciousness, if there are multiple such moments, such as a high-fidelity upload and the original person, who remember the same past identity equally well. A continuity identity theorist thinks that a person who gets uploaded and then dies is dead. A pattern identity theorist thinks that people die in that sense several times a second and have just gotten used to it. There are physical processes that correspond to moments of consciousness, but there's no physical process for linking two consecutive moments of consciousness as the same consciousness, other than regular old long and short term memories.

There's no question that the upload and the original will diverge. If I have a non-destructive upload done on me, I expect to get up from the upload couch, not wake up in the matrix, old habits and all that. And there is going to be a future me who will experience exactly that. But if the upload was successful, there's also going to be a future me who will be very surprised to wake up staring at some fluorescent polygons, having expected to wake up on the upload coach. This is where the "no unambiguous future selves" stops being sophistry and starts paying rent for the pattern identity theorist. "Which one is the real me" is a meaningless question. All we have to go with are memories, and both of me will have my memories.

If you want to argue a pattern identity theorist out of it, you'll want to argue why there has to necessarily be more than just memory going on with producing the sense of moment-to-moment personal continuity, and why the physically unconnected moments of consciousness model can't be sufficient.

Comment by Risto_Saarelma on January 2016 Media Thread · 2016-01-05T18:27:43.501Z · LW · GW

A review of Ernst Jünger's The Glass Bees.

Comment by Risto_Saarelma on January 2016 Media Thread · 2016-01-02T07:49:55.213Z · LW · GW

R. Scott Bakker: Crash Space

Comment by Risto_Saarelma on Voiceofra is banned · 2016-01-01T09:43:19.279Z · LW · GW

Yes, we do, maybe you'd notice if you didn't shut down your brain whenever you encountered a non-PC idea.

I don't think there's been much elaboration on the ideas that were already floating around here five-ish years ago in the last few years. We've just had the few regulars jumping in with the same message, failing to start much interesting conversation, and growing increasingly cranky.

Making being a reactionary your life's work isn't very rewarding. It's a feature of the present system that proponents who get boring and repetitive get thrown in the wood chipper and more clever and interesting ones take their place, but any single person will get stuck in their old material after a while.

Comment by Risto_Saarelma on Voiceofra is banned · 2015-12-31T06:40:50.940Z · LW · GW

Or because you and Jim are being tedious assholes nobody likes to hang out with, while going on about the same predictable set of not socially acceptable stuff for years and years without having anything new and interesting to say after a while.

Comment by Risto_Saarelma on Stupid questions thread, October 2015 · 2015-10-17T11:49:28.905Z · LW · GW

In Finland, today, can I just say "I don't feel like working" and get welfare for life?

(Not an expert on this stuff, but here's my rough understanding.)

You get a couple years of pretty straightforward welfare if you quit your job, then it looks like they will start doing means testing (tarveharkinta) on your savings and will stop paying you if it doesn't look like you're living hand-to-mouth. After you've gone through all your savings that the employment office is aware of, I think you can go on living in some sort of rental apartment and get food. There's also a spectrum of make-work programs from "send your application to this poorly matching open job we picked for you" to "attend this useless training course" to "rehabilitative labor activity" which can end up looking sort of like the American prisoner labor thing. The welfare will be suspended as a sanction if you refuse to attend, but I'm not quite sure how easy it is to end up actually homeless if you keep diligently pestering the social services and refuse to cooperate with anything work-like.

One problem is the diligent pestering of the social services part. Many of the actual unemployed are ill or have some mental problems, and they might not be that good at working the bureaucracy. So it probably helps if you're reasonably energetic and smart enough to navigate the systems of regulations if you want to become a lifestyle unemployed. Also, you need to make sure to spend your time in an economically unproductive way. Starting any kind of small business will wipe out all welfare eligibility instantly.

Comment by Risto_Saarelma on Open thread, Oct. 12 - Oct. 18, 2015 · 2015-10-16T17:49:41.561Z · LW · GW

Looks like you can just aim youtube-dl at the URL and it'll start downloading.

Comment by Risto_Saarelma on Open thread, Sep. 28 - Oct. 4, 2015 · 2015-10-04T15:40:51.642Z · LW · GW

If there was a large dataset of faces shot in a similar way and rated for attractiveness somewhere, you could take a photo of yourself, look for people in the set who look like you (possibly with some sort of face recognition program) and see how they are rated.

Comment by Risto_Saarelma on Open thread, Sep. 28 - Oct. 4, 2015 · 2015-10-04T15:29:39.320Z · LW · GW

I'm still doing this after starting a year ago. I've filled up one large ruled Moleskine and am 50 pages into the second one. I have calendar pages where I don't do any forward planning, but just write a one-line summary of what I worked on that day. Empty lines or variants of "slacking off" are an instant sign of trouble.

Other than that, the nice thing is just that I have a designated single nice journal to do any sort of brainstorming notes I need. Random ideas, planning an ongoing project or reading notes all just start by labeling a new page on the journal and writing down whatever is relevant.

Comment by Risto_Saarelma on Open thread, Sep. 28 - Oct. 4, 2015 · 2015-10-04T15:16:06.144Z · LW · GW

Not exactly, but related: Hugh Everett's' daughter Elizabeth committed suicide in 1996 and wrote in her suicide note that she's going to a parallel universe to be with her father.

Comment by Risto_Saarelma on Open thread, Sep. 28 - Oct. 4, 2015 · 2015-10-04T15:10:36.136Z · LW · GW

It's still related to his shtick and people are getting really tired of his shtick.

Comment by Risto_Saarelma on The Best Textbooks on Every Subject · 2015-09-30T11:10:55.073Z · LW · GW

No, it's just indicating that I haven't made any sort of concentrated effort at clearing my reading list or maintaining some sort of FIFO discipline on it. The Complete History of the World in Impeccable Engaging Detail tends to not do very well against a Warren Ellis comic book about shooting aliens wearing human skin suits in the head with flesh-eating bullets when picking random media to consume during idle time.

Comment by Risto_Saarelma on The Best Textbooks on Every Subject · 2015-09-28T12:34:30.692Z · LW · GW

Can't recommend a book I've read, but I've had J.M. Roberts' The New Penguin History of the World on my reading list for a while now. It's more big picture than facts.

If you're after rulers, dates and the like, just diving into wikipedia, starting from high-level articles and taking your own notes might not be a terribly bad approach.

Comment by Risto_Saarelma on [Link] Marek Rosa: Announcing GoodAI · 2015-09-17T13:38:45.632Z · LW · GW

I'd be happy if there was a RSS feed of his publicly visible FB posts.

Comment by Risto_Saarelma on September 2015 Media Thread · 2015-09-06T08:43:40.578Z · LW · GW

Stand Still, Stay Silent, a webcomic about a post-apocalyptic Northern Europe with very nice art.

Comment by Risto_Saarelma on Stupid Questions September 2015 · 2015-09-05T13:19:36.444Z · LW · GW

Seconding this. I use the hledger variant.

Comment by Risto_Saarelma on Open Thread - Aug 24 - Aug 30 · 2015-08-27T09:34:15.204Z · LW · GW

It's probably a safe assumption that there exists some number of people dedicating their careers to the study of intelligence who are able to consider potential heritability confounders you can think up in five minutes.

Comment by Risto_Saarelma on Open Thread - Aug 24 - Aug 30 · 2015-08-25T08:24:29.840Z · LW · GW

Do you already have a track record of getting sizable groups of strangers doing things they wouldn't otherwise have done by influencing them on some other social media? Then it might be worth looking into how to game facebook.

If you don't, then the first question is if you should try to get into the social media influence game to begin with. How many people are trying to do it compared to people who have any traction with a number of followers, and what sets the successful people apart? If most people who don't bounce off right away are barely hanging by instead of becoming big and influential, how is life for them? How much is success driven by stuff like outrage clickbait, unrelenting smear jobs at whoever your opponent is, raising twitter lynch mobs and the like, and how comfortable would you be operating in an environment where those might be standard operating procedure?

Comment by Risto_Saarelma on Ideas on growth of the community · 2015-08-15T09:47:35.289Z · LW · GW

Funny thing, the previous person with minimal earlier site presence who came in with "here's how to start properly growing Less Wrong" was also kind of tone-deaf and annoying.

Comment by Risto_Saarelma on August 2015 Media Thread · 2015-08-05T18:44:49.659Z · LW · GW

I just found out that some comic books I read in Finnish in the 80s were originally published in English in 1976 in a magazine called Starstream. I re-read the comics, which are an anthology of comic adaptations of various golden age SF short stories. They also mostly stick to the source material, such as John Campbell's Who Goes There, which was also the basis for John Carpenter's The Thing. Generally it's quite a bit better than what you'd expect from "newsstand comic book from 1976", and a lot of the stories are quite weird, from the mix of outdated science and narrative conventions, source material from authors who sometimes were actually very good and the general mismatch with what you'd expect from the dated comic book format. Robert Silverberg, Isaac Asimov, Robert Bloch, Poul Anderson and Theodore Sturgeon are some of the more notable authors who get an adaption.

Comment by Risto_Saarelma on Open Thread, Jul. 27 - Aug 02, 2015 · 2015-07-28T11:33:56.077Z · LW · GW

Obviously the solution is a smartwatch which pushes retractable needles in a pattern that tells the current time in binary into the skin of your wrist once every minute.

Comment by Risto_Saarelma on Open Thread, Jul. 20 - Jul. 26, 2015 · 2015-07-25T07:36:18.411Z · LW · GW

Turns out there is. Probably not all of the programs though.

Are you trying to do something specific or are you just curious about learning about Bayesian statistics? The software on that list probably won't be that useful unless you already know a bit about statistics theory and have a specific problem you want to solve.

Comment by Risto_Saarelma on Beyond Statistics 101 · 2015-06-27T18:00:51.052Z · LW · GW

It has seemed to me that a lot of the commenters who come with their own solid competency are also less likely to get unquestioningly swept away following EY's particular hobbyhorses.

Comment by Risto_Saarelma on Beyond Statistics 101 · 2015-06-27T13:03:57.233Z · LW · GW

There's also the whole Lesswrong-is-dying thing that might be contribute to the vibe you're getting. I've been reading the forum for years and it hasn't felt very healthy for a while now. A lot of the impressive people from earlier have moved on, we don't seem to be getting that many new impressive people coming in and hanging out a lot on the forum turns out not to make you that much more impressive. What's left is turning increasingly into a weird sort of cargo cult of a forum for impressive people.

Comment by Risto_Saarelma on Lesswrong, Effective Altruism Forum and Slate Star Codex: Harm Reduction · 2015-06-10T09:38:10.023Z · LW · GW

Did any of the really valuable contributors to LW go away because they were driven away by incessant criticism? You think Scott Alexander moved to SSC because he couldn't handle the downvotes?

Didn't Eliezer say somewhere that he posts on Facebook instead of LW nowadays because on LW you get dragged into endless point-scoring arguments with dedicated forum arguers and on Facebook you just block commenters who come off as too tiresome to engage with from your feed?

Comment by Risto_Saarelma on Stupid Questions May 2015 · 2015-05-04T16:42:19.321Z · LW · GW

Mathematicians have come up with formal languages that can, in principle, be used to write proofs in a way that they can be checked by a simple algorithm. However, they're utterly impractical.

I understood that a part of the univalent foundations project is to develop a base formalism for mathematics that's amenable to similar layered abstraction with formal proofs as you can do with programs in modern software engineering. The basic formal language for proofs is like raw lambda calculus, you can see it works in theory but it'd be crazy to write actual stuff in it.

So is it possible that in the future we might be able to have something that's to the present raw proof languages as Haskell is to basic lambda calculus, and that it might actually be feasible to write proofs on top of established theorem libraries with the highest level of proof code concise enough for comfortable human manipulation?

I also understand that Coq does some limited proof search based on the outline given by the human operator, which is another interesting usability groove on top of the raw language. Of course both using a complex, software-engineering like theorem library and giving proof-hints to a Coq style program are pretty obvious expert skills which you'll expect to have after being quite familiar with knowing how mathematical proofs work in general.

Comment by Risto_Saarelma on Stupid Questions May 2015 · 2015-05-03T06:08:06.830Z · LW · GW

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.

Comment by Risto_Saarelma on How to sign up for Alcor cryo · 2015-04-27T05:02:25.175Z · LW · GW

Any success stories for signing up for cryonics for people with middle-class wealth who don't have a citizenship in an Anglosphere country?

Comment by Risto_Saarelma on April 2015 Media Thread · 2015-04-02T17:53:07.890Z · LW · GW

Peter Watts on Person of Interest.

Comment by Risto_Saarelma on How has lesswrong changed your life? · 2015-04-01T10:52:41.143Z · LW · GW

I've learned that it's probably optimal to strive for the most high-earning high-productivity career you can accomplish and donate your extra income to effective altruism and that I'm not going to go and try to do that.

Comment by Risto_Saarelma on HPMOR Q&A by Eliezer at Wrap Party in Berkeley [Transcription] · 2015-03-19T14:14:36.636Z · LW · GW

Voldemort gave Snape a vision of him performing procedure 110 Montauk on Lily