Nnews
I
M
A
G
E
B
Y
I
N
D
U
C
T
I
V
E
L
O
A
D
Automating Proofs
Math struggles with the usability of formal proofs.
OVER THE PAST two decades, mathematicians have succeeded in bringing computers to bear on the development of proofs
for conjectures that have lingered for
centuries without solution. Following
a small number of highly publicized
successes, the majority of mathematicians remain hesitant to use software
to help develop, organize, and verify
their proofs.
Yet concerns linger over usability and the reliability of computerized
proofs, although some see technological assistance as being vital to avoid
problems caused by human error.
Troubled by the discovery in 2013 of
an error in a proof he co-authored almost 25 years earlier, Vladimir Voevod-sky of the Institute for Advanced Study
at Princeton University embarked on a
program to not only employ automated proof checking for his work, but to
convince other mathematicians of the
need for the technology.
Jacques Carette, assistant professor in the department of computing
and software at McMaster University
in Ontario, Canada, and a promoter
of the idea of ‘mechanized mathematics’, says, “There are both technical
and social forces at work. Even though
mathematicians doing research are
trying to find new knowledge, they are
quite conservative about the tools they
Science | DOI: 10.1145/2892710 Chris Edwards
An example of a four-color map. The four-color map theorem says no more than four colors
are required to color the regions of a two-dimensional map so no two adjacent regions have
the same color.
