Finding a proof or a counter example in a programming puzzle Some years ago I entered a programming contest and this was one of the problems:
Binary Granny
Summary: Given a positive integer N find 2 positive integers such that $$ x + y = N $$Let X and Y be the number of
bits set in the base 2 representation of x and y respectively(Hamming weight of x and y). Maximize X + Y.
For some reason I had a hard time at first in python(mostly because I was using an stupid algorithm that was too slow with large N) so I decided to try to solve it using Haskell. Eventually I managed to solve it somehow with very good performance with this Haskell code:
import IO
import Control.Monad

read_number_of_cases :: IO Integer

read_number_of_cases = do
    s <- getLine
    let number_of_cases = read s :: Integer
    return number_of_cases

main :: IO ()

main = do
    hSetBuffering stdin LineBuffering
    number_of_cases <- read_number_of_cases
    forM_ [1..number_of_cases] (\i -> do
        line <- getLine
        let number = read line :: Integer
            a000120 0 = 0
            a000120 n = a000120 n' + m where (n', m) = divMod n 2
            middle = if even number
                     then truncate(toRational(number)/2)::Integer
                     else truncate(toRational(number)/2)::Integer
            max_p1 = if (a000120 middle)>=(truncate(logBase 2 (fromIntegral middle))+1)
                     then middle
                     else truncate(2**fromIntegral(truncate(logBase 2 (fromIntegral middle)))-1)
            max_p2 = if (a000120 number)>=(truncate(logBase 2 (fromIntegral number))+1)
                     then number
                     else truncate(2**fromIntegral(truncate(logBase 2 (fromIntegral number)))-1)
            result = if max_p1 > max_p2
                     then a000120(max_p1) + a000120(number - max_p1)
                     else a000120(max_p2) + a000120(number - max_p2)
        putStrLn ("Case #"++show i++": "++(show result)))`

(A000120 calculates the Hamming weight https://oeis.org/A000120)
What this code does is:
$$
    middle = \left\lfloor {\frac{N}{2}} \right\rfloor\\
max_{p1}=\begin{cases}
    middle,& \text{if } Hamming(middle)\geq \left\lfloor log_2(middle) \right\rfloor + 1\\
    \left\lfloor 2^{ \left\lfloor (log_2(middle) )\right\rfloor}-1 \right\rfloor,              & \text{otherwise}
\end{cases}\\
max_{p2}=\begin{cases}
    middle,& \text{if } Hamming(N)\geq \left\lfloor log_2(N) \right\rfloor + 1\\
    \left\lfloor 2^{ \left\lfloor (log_2(N) )\right\rfloor}-1 \right\rfloor,              & \text{otherwise}
\end{cases}\\
result=\begin{cases}
    Hamming(max_{p1})+Hamming(N-max_{p1}),& \text{if } max_{p1} \gt max_{p2} \\
    Hamming(max_{p2})+Hamming(N-max_{p2}),              & \text{otherwise}
\end{cases}
$$
That worked, but to be honest I have no idea why, or if it would work for every case.
So the question is: Is there an easy way to prove that it is correct? Or incorrect if that is the case?
 A: It may be better to use math instead of computing power.
If $N=2M+1$ is odd, then eactly one of $x,y$ must be odd and there is not carry in the least significant bit, that is the maximal weight sum of $x$ and $y$ for $N$ is exactly one more than for $M$.
If $N =2M$ is even there are two possibilities for our optimal $x$ and $y$: Either $x,y$ are both even and $x/2, y/2$ are optimal for $M$; or $x,y$ are both odd and $(x-1)/2$, $(y-1)/2$ (which have one bit less each) are optimal for $M-1$ (watch the carry).
We conclude that
$$\tag1 f(N)=\begin{cases}2&\text{if $N=2$ or $N=3$}\\f(\tfrac {N-1}2)+1&\text{if $N>3$ is odd}\\
\max\{f(\tfrac {N}2),f(\tfrac{N-2}2)+2\}&\text{if $N>3$ is even}\end{cases}$$
This is already a nice way to tackle the problem with dynamic programing. 
But the max in the last case looks ugly.
Proposition. $f(n+1)\le f(n)+1$ for all $n\ge 2$.
Proof.
Let $n+1=x+y$ be a maximal weight sum decomposition of $n+1$. Then wlog $x\ge 2$ (as $n+1\ge 3$), and the weight of $x-1$ is bounded by  $\operatorname{wt}(x-1)\ge \operatorname{wt}(x)-1$, hence $f(n)\ge\operatorname{wt}(x-1)+\operatorname{wt}(y)\ge \operatorname{wt}(x)+\operatorname{wt}(y)=f(n)$. $_\square$
From the proposition we can simplify $(1)$ to 
$$\tag2 f(N)=\begin{cases}2&\text{if $N=2$ or $N=3$}\\f(\tfrac {N-1}2)+1&\text{if $N>3$ is odd}\\
f(\tfrac{N-2}2)+2&\text{if $N>3$ is even}\end{cases}$$
This gives a method to calculate $f(N)$ in $O(\log(N))$ steps. In fact, you may observe a simple formula that uses only the bit length of $N-1$ and the Hamming weight of $N-1$. Also, cf. A014701
