If you’ve read Brouwer or Heyting, you’ve probably seen examples involving the question if 0123456789 occurs in the decimal expansion of π. I wasn’t aware that it’s been known for a few years that it does: the first time at the 17,387,594,880th digit. There’s also 10 consecutive 7’s starting at 22,869,046,249.
…and the one about not knowing constructively whether there are irrationals x and y such that x^y is rational, and the *30* *years* out of date claim that there’s a completeness result for intuitionistic logic but no constructive proof of it… Posted by Charles Stewart
This ‘only’ goes up to 200 million digits, so it doesn’t answer your two questions, but it is very cool nonetheless! Posted by Nick Smith