I broadly agree with the gears to ascension’s complaint. The title and first paragraph of the post were pretty appealing (I’d love to read a post exploring how a superhuman theorem prover could be usefully applied to alignment research), but to that end, the post was quite disappointing.
For the purpose of this exercise, assume that you have an oracle that takes as input a math problem stated with about the level of rigor of a Math Olympiad problem, converts it into a formal specification, creates a formal proof, and then generates a human readable summary of that proof.
Is a highly non-trivial assumption for most of the use cases you highlighted. Some of them I don’t expect to be practically formalisable without a strongly superhuman general intelligence.
Some I’m not sure can be rigorously formalised by physically feasible systems.
This was not intended to be a practical list. It was intended to refute the claim “mathematical provers… would not help at all”
I estimate only like 2-3 of these are “practical” with systems that will be built before the singularity.
But not 0 of them.
And if you have a boxed super-intelligent theorem-proving AGI I would guess most of them are within reach.
Perhaps I should write a 2nd “list of practical things I might do with a Proof Oracle”. But given that I’m at −9 karma for this post, not really sure it’s worth it.
I broadly agree with the gears to ascension’s complaint. The title and first paragraph of the post were pretty appealing (I’d love to read a post exploring how a superhuman theorem prover could be usefully applied to alignment research), but to that end, the post was quite disappointing.
Is a highly non-trivial assumption for most of the use cases you highlighted. Some of them I don’t expect to be practically formalisable without a strongly superhuman general intelligence.
Some I’m not sure can be rigorously formalised by physically feasible systems.
This was not intended to be a practical list. It was intended to refute the claim “mathematical provers… would not help at all”
I estimate only like 2-3 of these are “practical” with systems that will be built before the singularity.
But not 0 of them.
And if you have a boxed super-intelligent theorem-proving AGI I would guess most of them are within reach.
Perhaps I should write a 2nd “list of practical things I might do with a Proof Oracle”. But given that I’m at −9 karma for this post, not really sure it’s worth it.