Given all the Lean4 AI proofs, I thought I'd dabble with that a bit myself.
Formalisations matter, as I learned the hard way during my PhD studies. It's completely possible that a formalisation works out on paper, but is 'impossible' to work with in an interactive theorem prover.
So, I thought I'd revisit possibly infinite streams in Lean4 and came up with the formalisation below. But I now think I should reject it as 'another wrong attempt at formalising a co-inductive type.'
A series is a set of lists closed under prefix that shares all prefixes.
No comments:
Post a Comment