Stream: new members
Huỳnh Trần Khanh (Jan 16 2021 at 14:01):
I want to prove that this code solves this problem. It's a "dynamic programming" solution to that problem. It seems that recursive stuff can be proven using induction so I guess I have to use induction in one way or another but how do I represent the binary representations of natural numbers and how do I generate a list of binary representations of natural numbers in the range [1, n]?
Kevin Buzzard (Jan 16 2021 at 14:03):
I'm not a computer programmer. But my guess is that what you're asking right now is very hard, and it might be easier if you were to write code in Lean itself which solves the problem, rather than in C or C++ or whatever that code is written in.
Kevin Buzzard (Jan 16 2021 at 14:04):
Lean is a functional programming language as well as an interactive theorem prover.
Last updated: May 15 2021 at 23:13 UTC