Many of these do not seem to be easily specified true/false statements in formal mathematical logic. I don’t think I can prove a theorem which allows me to arbitrage the market, unless there’s some derivatives contract tied to the existence of a mathematical proof without first knowing what the theorem is I’m trying to prove. Even then, finding such a theorem would be the hard part.
More centrally: many have been working on a formal specification of the diamond alignment problem for years. That is not to say that you couldn’t do it, but an AI that can accomplish such a task would not be a mere theorem prover.
It’s neither. I’m claiming you need more than just a theorem prover’s mental skills to accomplish the task. If you think you can formulate the specification in formal mathematical logic, so that you do only need a theorem prover to accomplish the task (and also a list of possible programs), then go ahead. I’d be excited if you succeeded.
Many of these do not seem to be easily specified true/false statements in formal mathematical logic. I don’t think I can prove a theorem which allows me to arbitrage the market, unless there’s some derivatives contract tied to the existence of a mathematical proof without first knowing what the theorem is I’m trying to prove. Even then, finding such a theorem would be the hard part.
More centrally: many have been working on a formal specification of the diamond alignment problem for years. That is not to say that you couldn’t do it, but an AI that can accomplish such a task would not be a mere theorem prover.
Can’t tell if this is a job offer or an argument of the form “I tried this and failed therefore it is impossible”
It’s neither. I’m claiming you need more than just a theorem prover’s mental skills to accomplish the task. If you think you can formulate the specification in formal mathematical logic, so that you do only need a theorem prover to accomplish the task (and also a list of possible programs), then go ahead. I’d be excited if you succeeded.