Geared with increasingly fast computer algebra libraries and
scientific computing software, computers have become amazing
instruments for mathematical guesswork. In fact, computer calculations
are even sometimes used to substantiate actual reasoning steps in
proofs, later published in major venues of the mathematical
literature. Yet surprisingly, little of the now standard techniques
available today for verifying critical software (e.g., cryptographic
components, airborne commands, etc.) have been applied to the programs
used to produce mathematics. In this talk, we propose to discuss this
state of affairs
Copyright. All Rights Reserved.