dernett

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 construct a `Fin n` instance.

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.

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 equivalent way of looking at a != b.

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 advocates for itself...

Is it possible to create animations using something like Shadertoy's `iTime`?

This is really helpful. Minor nit under Curry-Howard correspondence: "True propositions have exactly one term" should be "have at least one term".

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.