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.
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.