Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in this abstract that this was an open problem. However, it was already known that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new?

Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to Bauer's blog.

Edit: Thanks to the answers by Andrej Bauer and James Hanson, I have realized my biggest misunderstanding. I for some reason implicitly thought subcountability and countability are equivalent, but this is not the case in the intuitionist setting. Thus, the consistency of the Dedekind reals being subcountable does not yield that it is consistent that the Dedekind reals are countable.

Something else several others pointed out is that CZF is a generally weaker system than "ZFC without choice or LEM". So, even if the question were to be solved in CZF, this wouldn't mean the question "Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?" was really settled. Bauer's and Hanson's topos construction gives a negative answer in the setting of higher-order intuitionist logic.

Thanks again to everyone for sharing your input!

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in this abstract that this was an open problem. However, it was already known that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new?

Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to Bauer's blog.

Edit: Thanks to the answers by Andrej Bauer and James Hanson, I have realized my biggest misunderstanding. I for some reason implicitly thought subcountability and countability are equivalent, but this is not the case in the intuitionist setting. Thus, the consistency of the Dedekind reals being subcountable does not yield that it is consistent that the Dedekind reals are countable.

Something else several others pointed out is that CZF is a generally weaker system than "ZFC without choice or LEM". So, even if the question were to be solved in CZF, this wouldn't mean the question "Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?" was really settled. Bauer's and Hanson's topos construction gives a negative answer in the setting of higher-order intuitionist logic (and in IZF as per Hanson's comment).

Thanks again to everyone for sharing your input!

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in this abstract that this was an open problem. However, it was already known that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new?

Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to Bauer's blog.

Last year, Andrej Bauer gave a talk showing that there is a topos in which the set of Dedekind reals is (sub)countable, and thus, you cannot prove that $\mathbb{R}$ is uncountable without LEM. He claims in this abstract that this was an open problem. However, it was already known that it is consistent with CZF that every set (and in particular, the Dedekind reals) is subcountable. So is Bauer's and Hanson's result actually new?

Also note that Bauer's and Hanson's result is not yet published, but it should supposedly be published soon according to Bauer's blog.

Edit: Thanks to the answers by Andrej Bauer and James Hanson, I have realized my biggest misunderstanding. I for some reason implicitly thought subcountability and countability are equivalent, but this is not the case in the intuitionist setting. Thus, the consistency of the Dedekind reals being subcountable does not yield that it is consistent that the Dedekind reals are countable.

Something else several others pointed out is that CZF is a generally weaker system than "ZFC without choice or LEM". So, even if the question were to be solved in CZF, this wouldn't mean the question "Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?" was really settled. Bauer's and Hanson's topos construction gives a negative answer in the setting of higher-order intuitionist logic.

Thanks again to everyone for sharing your input!