Computers are widely used as observation instruments for testing and refining conjectures, in a broad range of mathematical areas. They actually even substantiate actual proof steps in published proofs. In particular, a large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation, and the potential of proof assistants based on dependent types.