Though note that that True/False machine could also quickly lead to the discovery of actual proofs, for example by making it extremely efficient to search for counterexamples. "The Collatz conjecture is true for all n ≤ some_huge_number." Also perhaps by making it extremely efficient to search for correct proofs in a lexicographically ordered list of proofs. "The shortest valid proof of the Collatz conjecture in the list of all proofs in my formalism is before proof number some_huge_number."

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?