IMO challenge bet with Eliezer — LessWrong