dernett

6 ms·

1.
by dernett 7mo ago
Not sure about Idris, but in Lean `Fin n` is a struct that contains a value `i` and a proof that `i < n`. You can read in the value `n` from stdin and then you can do `if h : i < n` to have a compile-time proof `h` that you can use to
2.
by dernett 8mo ago
This is crazy. It's clear that these models don't have human intelligence, but it's undeniable at this point that they have _some_ form of intelligence.
3.
by dernett 9mo ago
Lean defines a != b as a = b => False, so it seems that we have a function from proofs of a = b to proofs of False. I guess this being bijective means that there are no proofs of a = b, since there are no proofs of False, which is an equ
4.
Microarchitecture: What Happens Beneath [video](youtube.com)
2 points by dernett 9mo ago|0 comments
5.
by dernett 1y ago
This really sounds like it was generated by an LLM. "X isn't a Y. It's a Z", examples that don't make any sense (why would it think you're a farmer?), etc. Perhaps not the most surprising thing that an LLM advo
6.
by dernett 1y ago
Is it possible to create animations using something like Shadertoy's `iTime`?
7.
by dernett 1y ago
I'm going to try formalizing this course in Lean--not sure how hard it is going to be. If anyone is interested in doing the same, please feel free to contribute! https://github.com/dernett/Lean61200J
8.
by dernett 1y ago
I'm assuming he's talking about this specific small string optimization: https://www.youtube.com/watch?v=kPR8h4-qZdk&t=409s
9.
by dernett 1y ago
This is really helpful. Minor nit under Curry-Howard correspondence: "True propositions have exactly one term" should be "have at least one term".
10.
by dernett 4y ago
I don't believe so. I worked out the permutations for n = 3 and, accounting for rotations, you only get 2: [0, 3, 4, 1, 2, 5] [0, 5, 2, 1, 4, 3]. Of course, you get the expected answer of 12 if you multiply by 6.