Freek's class on Proof Assistants
Sep. 30th, 2004 03:29 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslI've been following a class on Proof Assistants.
Yesterday I first created definitions and real proofs in Coq. It's easier than I thought, and really cool that I can do it. We defined the natural numbers as S* 0, and from there we defined there addition, multiplication, and then a type "list of naturals", and then the "append" operation on lists... one of the theorems was showing that length (append x y) = plus (length x) (length y).
Tuesday morning I spoke to Freek about the possibility of formalizing stuff from the theory of Kolmogorov Complexity. It seems there would be a lot of background material to formalize, regarding computability theory, etc. which would apparently be a slow and costly process.
Another direction we're looking at are educational applications.
Yesterday I first created definitions and real proofs in Coq. It's easier than I thought, and really cool that I can do it. We defined the natural numbers as S* 0, and from there we defined there addition, multiplication, and then a type "list of naturals", and then the "append" operation on lists... one of the theorems was showing that length (append x y) = plus (length x) (length y).
Tuesday morning I spoke to Freek about the possibility of formalizing stuff from the theory of Kolmogorov Complexity. It seems there would be a lot of background material to formalize, regarding computability theory, etc. which would apparently be a slow and costly process.
Another direction we're looking at are educational applications.