Comments on: Ask Me Anything

By: Google Buys Quantum Computer Lab | Pink Iguana

Google Buys Quantum Computer Lab | Pink Iguana — Thu, 16 May 2013 12:35:30 +0000

[...] edition of “Ask Me Anything.” (For the previous editions, see here, here, here, and here.) Today’s edition is partly to celebrate my new, tenured “freedom to do whatever the hell I [...]

By: Shtetl-Optimized » Blog Archive » Ask Me Anything! Tenure Edition

Shtetl-Optimized » Blog Archive » Ask Me Anything! Tenure Edition — Mon, 06 May 2013 14:43:01 +0000

[...] edition of “Ask Me Anything.” (For the previous editions, see here, here, here, and here.) Today’s edition is partly to celebrate my new, tenured “freedom to do whatever the [...]

By: Ask me anything « knitnut.net

Ask me anything « knitnut.net — Tue, 11 Sep 2012 13:39:27 +0000

[...] Subject-wise, anything goes. Just don’t ask me about stuff like transhumanism and its relation to quantum computing, or the hardness of simulating Newtonian physics. [...]

By: Links « Front to Back Books

Links « Front to Back Books — Thu, 12 Jan 2012 11:18:56 +0000

[...] Aaronson’s blog on Quantum computing, Shtetl-Optimized, boarders on required reading - Ask Me Anything is good where he answers any and all questions posed to him over a span of days – but just [...]

By: helpneeded

helpneeded — Tue, 20 Sep 2011 05:51:15 +0000

I thought more about it. I found why it failed. So I won the challenge:)

By: helpneeded

helpneeded — Sat, 17 Sep 2011 08:25:22 +0000

I mean ‘gave me a rank deficient matrix’ not a ‘deficient work’.

By: helpneeded

helpneeded — Sat, 17 Sep 2011 08:24:33 +0000

The MM attempt failed. I am very very surprised though!! I have not seen this approach. Not because the complexity is bad. But the one choice of parameters I could make the complexity work gave me a deficient work. It is very elementary. But I have not seen this method before in my literature search starting from 1970. I could probably have figured it out earlier if I had a fully loaded Mathematica! Would you be interested in atleast taking a look? I have a certain feeling it is a totally different approach than you most likely would have seen before!! I do not know whether to give up or not since the literature search also came out empty but the matrices involved have so much structure.

By: Shiri Dori-Hacohen

Shiri Dori-Hacohen — Fri, 02 Sep 2011 21:44:08 +0000

Very late to the game, but just wanted to mention re: #259, even though I agree with Warren Buffett as a choice, I highly doubt that he would resign Berkshire-Hathaway to step up! He likes what he does way too much. All in all, great Q&A session!

By: Scott

Scott — Wed, 24 Aug 2011 14:53:30 +0000

Neel #272:

As an aside, MIT just hired Adam Chlipala, who is another expert on using proof assistants. You might enjoy talking with him.

I’ve already had some very enlightening conversations with him and hope to have more!

By: Neel Krishnaswami

Neel Krishnaswami — Wed, 24 Aug 2011 13:56:11 +0000

For more of a “challenge,” how about the Classification of Finite Simple Groups?

No smiley needed: I’m down the hall from George Gonthier, who is working on precisely this problem. It’s actually an excellent test problem for machine-checked proof, because it’s (a) enormous, and (b) one of the pinnacles of modern mathematics. The first point means that if you can handle it, you know you aren’t missing some critical feature needed for modular proof development, and the second point means that your proof assistant can formalize all the really wild tricks that mathematicians have thought up.

As an aside, MIT just hired Adam Chlipala, who is another expert on using proof assistants. You might enjoy talking with him.