# Professor Freek Wiedijk

The PhysOrg article
*Proof by computer: Harnessing the
power of computers to verify mathematical proofs* said

New computer tools have the potential to revolutionize the practice of mathematics by providing far more-reliable proofs of mathematical results than have ever been possible in the history of humankind. These computer tools, based on the notion of “formal proof”, have in recent years been used to provide nearly infallible proofs of many important results in mathematics. A ground-breaking collection of four articles by leading experts, published today in theNotices of the American Mathematical Society, explores new developments in the use of formal proof in mathematics.

When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible. When it comes to central, well known results, the proofs are especially well checked and errors are eventually found. Nevertheless the history of mathematics has many stories about false results that went undetected for a long time.

In addition, in some recent cases, important theorems have required such long and complicated proofs that very few people have the time, energy, and necessary background to check through them. And some proofs contain extensive computer code to, for example, check a lot of cases that would be infeasible to check by hand. How can mathematicians be sure that such proofs are reliable?

To get around these problems, computer scientists and mathematicians began to develop the field of formal proof. A formal proof is one in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. Mathematicians do not usually write formal proofs because such proofs are so long and cumbersome that it would be impossible to have them checked by human mathematicians. But now one can get “computer proof assistants” to do the checking. In recent years, computer proof assistants have become powerful enough to handle difficult proofs.

Freek Wiedijk, Ph.D. was one of these four ground-breaking experts
and is Assistant Professor of Computing and Information Sciences
at Radboud Universiteit Nijmegen, The Netherlands.
Freek says “For my American friends: the name Freek is pronounced like
‘Phrake’.
It’s a perfectly ordinary Dutch name (from Frederic), no reference to
freak was ever intended. And ‘Wiedijk’ is pronounced like ‘Weedike’.”

Freek is a mathematician (without a specialization, but with a fondness
for
algebraic and topological subjects).
His
M.Sc. thesis was about the geometry of supergravity (that’s mathematical
physics) and his Ph.D. thesis in 1990 at the University of Amsterdam was
about conservativity in
modular
specifications (that’s mathematical computer science.)

He edited
*The Seventeen Provers of the World: Foreword by Dana S. Scott
(Lecture
Notes in Computer Science / Lecture Notes in Artificial
Intelligence)*,
and coedited
*Types for Proofs and Programs: Second International Workshop, TYPES
2002, Berg en Dal, The Netherlands, April 24–28, 2002, Selected
Papers* and
*Intelligent Computer Mathematics: 9th International Conference, AISC
2008 15th Symposium, Calculemus 2008 7th International Conference, MKM
2008 Birmingham (Lecture Notes in Computer
Science)*.

Freek authored
*Formal Proof — Getting
Started*,
*Mizar’s Soft Type System*,
*The QED Manifesto Revisited*,
*Is ZF a hack? Comparing the complexity of some (formalist
interpretations of) foundational systems for mathematics*, and
*On the usefulness of formal methods*,
and coauthored
*Deduction using the ProofWeb system*,
*Teaching logic using a state-of-the-art proof assistant*,
*Certified Computer Algebra on top of an Interactive Theorem
Prover*,
*Constructive analysis, types, and exact real numbers*,
*The Challenge of Computer Mathematics*,
*The meaning of infinity in calculus and computer algebra
Systems*, and
*C-CoRN, the Constructive Coq Repository at Nijmegen*.

Read *Digital Math by
Alphabet*,
*Do you agree… Ten Questions about Intuitionism*,
Download
Lambda calculus and CL reduction tool by Freek Wiedijk.