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...
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!