Robust computer algebra, theorem proving, and oracle AI