Scott Garrabrant's problem on recovering Brouwer as a corollary of Lawvere — LessWrong