Binary counting is hard

Michaël Cadilhac recently (on Autoboz) asked the following problem: Take n > 0 and consider the alphabet A_n = { 2^i | i ≤ n }. Let L_n be the set of words over A_n that sum up to 2^n. What is the size of the minimal context-free grammar which recognises L_n? The problem is motivated by linear programs, compression algorithms, and some questions of automata with binary counters. Together with Michaël Cadilhac, Arka Ghosh, and Michał Pilipczuk we managed to provide a handy answer to the problem. During the talk I will just give you the meat, i.e. an argument for lower and upper bounds. In return, I will gladly learn about possible applications of the result :)