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 the Notices 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.