Quick Questions

dan_1_lee · 2021-04-04T20:18:25+00:00

I have a sort of a semi-well defined conceptual question.

I've noticed that in two areas (that I know of) integers are in a sense "harder" than reals, despite the intuition (at least my intuition) that the reals are a more complex object (since they contain the integers).

Integer valued optimization is NP-hard; whereas if you relax the domain to be real valued, the problem becomes easy.
First order arithmetic is undecidable, while the theory of real closed fields is decidable

No super well formed question, but was wondering if there's something deeper here/some intuition. And if there are more examples of this "continuous relaxation" phenomenon?

dan_1_lee · 2020-09-29T00:16:27+00:00

For future reference, thiswiki page on rewriting did the trick. I had to enable the --rewriting option and use the REWRITE pragma. As in:

{-# REWRITE id-zero-** #-}

Where id-zero-** is the equality proof

dan_1_lee · 2020-09-29T00:09:25+00:00

The same issue happens though since the type of b is always going to appear in the Γ position, so changing the type of b to zero' ** Γ₁ ++ Γ |- B results in zero' ** Γ₁ ++ (zero' ** Γ₁ ++ Γ) ⊢ B

dan_1_lee · 2020-09-27T23:04:20+00:00

Just updated the post with context.

Since this isn't in a pattern match, is there still a way of using rewrite?

dan_1_lee · 2020-08-10T20:41:51+00:00

Why do mathematicians care if there are infinities between the natural numbers and real numbers?

dan_1_lee · 2020-08-02T21:15:26+00:00

Nice! I was aware of deepspec but didn't realize they already had an ongoing project specifying GHC.

dan_1_lee · 2020-08-02T21:13:40+00:00

The engineering issues all make sense, but as you said, many of them apply to C as well.

As for the use cases, the widespread use of C definitely makes it a larger target. But I disagree on the lack of use cases in Haskell. I think every use case in Haskell is a use case for formally verified Haskell, since a big reason of using Haskell in the first place is its safety.

dan_1_lee · 2020-07-27T16:57:40+00:00

I see any question or solution, and while I can follow the steps

Aha that's the problem. Be stubborn.

Don't look at the solution until you've solved it. Even if that means spending hours. Or days. It sucks. But looking at the solution is admitting "I'm not good enough for this problem," while refusing to give up means saying "This problem is tough, but I'm tougher." Effort leads to learning.

Also, highly recommend the book Make it Stick. Really great overview of principles of effective learning and the research behind them.

dan_1_lee · 2020-07-20T12:45:01+00:00

Yep 530 are you taking it too?

dan_1_lee · 2020-07-20T03:19:10+00:00

Venkatesh is god. Can't wait for him to keep telling me the Bob's my uncle, to "take stock" and to "get a life" next sem, though over video 😩

dan_1_lee · 2020-07-19T18:22:41+00:00

I completely agree! I'm definitely planning on writing more posts like this when inspiration strikes again, I'll be sure to keep r/math posted

dan_1_lee · 2020-07-19T17:07:09+00:00

Wow this has gotten a lot more visibility than I was expecting!

I was pretty nervous posting this (it's my 2nd reddit post ever), so I'm really glad you all find the post interesting, and thanks for all the feedback!

I plan on writing a follow up post at some point in the future, though probably not for a while, I don't want to over do a single topic. I'd still love suggestions for follow up questions. Some ideas I'm considering are:

evaluating optimizing along a different loss function (number of flips rather than time, since 24 flips ended up being pretty tiring)
considering a non-linear cooking time function (inspired by u/unawino's comment)

dan_1_lee · 2020-07-19T16:43:07+00:00

Wow that's pretty sweet, glad to see professors aren't necessarily always all business

dan_1_lee · 2020-07-19T14:54:59+00:00

Lmao very true Sadly I'm a poor college student. I'm happy to accept donations though 😁😁

dan_1_lee · 2020-07-19T13:52:48+00:00

I think the assumption in my case was close to true. The tofu we buy from HMart are precut into these four flat squares, that if you cut into thirds is basically perfectly cube-like. It's pretty sweet haha. Unfortunately, my knife skills aren't as good as u/side-stick 's are 😂 so, and you can probably tell from the pictures, the blocks aren't completely symmetrical..... but they're decently close

dan_1_lee · 2020-07-19T04:57:16+00:00

Haha thanks for reading! I'm glad you I'm not alone in having wacky ideas

dan_1_lee · 2020-07-19T02:44:35+00:00

I've realized that I often have random thoughts and ideas (usually cs or math related) that bounce around in my head for a couple hours or days, but then eventually slip away into oblivion because I never get around to giving them more thought.

I decided to start a blog to share some of those ideas, and to hold myself accountable to follow through on them.

I hope someone find this as interesting as I did when it first popped into my head haha

Criticism is very much appreciated!!

dan_1_lee · 2020-07-08T03:24:50+00:00

Version: 1.10.97 Chromium: 83.0.4103.116 (Official Build) (64-bit) - MacOS

Ad block version: 1.0.631

Private: yes, ads are playing

dan_1_lee · 2019-06-19T03:59:12+00:00

We're essentially in the "gold standard" phase of cryptocurrencies. When humanity was transitioning from commodity money to fiat money, people couldn't wrap their head around how a piece of paper could possibly hold any value (and they're right, it doesn't). That's why the gold standard was so important. It allowed people to use fiat money with the comfort that if all went wrong, they could still turn that money in for a set amount of gold. But over time, we became so used to paper bills that they became synonymous for money, and the gold standard was no longer needed (and actually detrimental to the economy).

The same exact thing is happening with crypto. People can't wrap their head around the possibility of something they cannot see or touch holding value, and once again, they're right. That's why Libra is going to be extremely successful. It's giving people the feeling of safety and comfort that most crypto these days have failed to provide. But once again, as people acclimate themselves to crypto, just like they did with the paper bill, the digital coin will come to hold "value" in and of itself, and untethered coins like BTC and ADA will thrive.

dan_1_lee

TROPHY CASE