Earlier quoted context omitted.
This is an excellent answer. I have a mostly unrelated question. In the case of the Collatz conjecture, it seems all but proved: > If the conjecture is false, it can only be because there is some starting number which gives rise to a sequence that does not contain 1. Such a sequence would either enter a repeating cycle that excludes 1, or increase without bound. No such sequence has been found. There are lots of hist…
They've verified that the Collatz conjecture holds for all numbers up to ~2^68, but that's precisely 0% of all the numbers that need to be checked. But more importantly, the goal of (pure) mathematics isn't to declare truths. If you had a machine from God himself that outputted True or False for theorems you put in, that wouldn't demotivate (pure) mathematicians from doing the work they're doing. Understanding the re…
Although I think the basic version of the machine is "just" the first Turing jump oracle
https://en.wikipedia.org/wiki/Turing_jump
-- it depends on how you formalize the inputs to the machine, right? -- so maybe mathematicians would still be busy afterward. :-) Maybe the machine is an oracle with infinite Turing degree?