# News from the world of maths: Automated mathematics

It may come as a surprise that your average proof in an academic journal is riddled with holes. Authors gloss over details, appeal to pictures, even intuition, and take hidden leaps of logical faith that, philosophically speaking, aren't entirely justified. These days mathematics contains proofs so long and complex that few people are able to check and understand them in full, yet once a result has made it through the peer review process and into a journal, its truth is taken as read.

All this is a far cry from the mathematical dream which started with Euclid over 2000 years ago: that every mathematical statement should be derived from the very axioms of mathematics in a sequence of verifiable logical steps. Proofs which do this are known as *formal proofs*, and they are the focus of a special issue of the *Notices of the American Mathematics Society*, which is
now freely available online.

Labels: Latest news

*posted by Plus @ 11:30 AM*