CSES Problem Set: Counting Bits

Stream: new members

[Huỳnh Trần Khanh]

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]

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]

Lean is a functional programming language as well as an interactive theorem prover.