:-) This is the personal home page of Freek Wiedijk.

In case you're looking for a way to reach me:

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".

*

I'm a mathematician (without a specialization, but with a fondness for algebraic and topological subjects), who tried to learn physics (and failed) and computers (love them, but only when they're not a mess.) My M.Sc. thesis was about the geometry of supergravity (that's mathematical physics) and my Ph.D. thesis was about conservativity in modular specifications (that's mathematical computer science.) After I got my Ph.D. I worked for six years as a system and network administrator at Utrecht University. I'm currently working in the project of Henk Barendregt and Herman Geuvers. I used to be a Coq programmer in the fundamental theorem of algebra project, and then I was a four-year postdoc. Currently I've become an assistant professor and at the moment I'm teaching a course about "formal thinking" for first year students, a course about computability for second year students, and a type theory and Coq course for master level students. I also am tutor of a small group of first year students. Finally I keep a weblog with interviews of our students (as propaganda for our study).

I don't have too many publications of my own (one of them is a comparison between provers), but I wrote several notes and I sometimes give talks. I authored one computer program: an Automath checker. It's portable (vanilla C), simple (3000 lines of code) and fast (on my current computer the test file which is Jutting's translation of a complete mathematical book gets checked in 0.6 seconds.) A simpler thing I authored is a small script called raft for doing proof developments with Otter. Something else I did: I compiled a list of computer math systems to investigate the state of the art in digital mathematics, which I have put on the web and will try to keep complete and up to date. And I wrote a small page about Mizar, which is a system for proof checking that deserves to be known much better than it is. I also wrote a page with a list of possible proof checking projects. And then I have a page which investigated which of a list of 100 theorems have been formalized in which systems. Finally, I organised a session with proof assistant demos at ICMS 2006.

I also scanned Brouwer's notebooks (from his PhD period) together with John Kuiper.

I'm living (with elfish friend and big son – a great source of passwords – and small son and daughter and far too many mice) in three very small and unfinished but quite tranquil apartments, right next to the Zuiderkerk in Amsterdam. Sometimes I'm not there. Then I'm somewhere else.

I've lots of ways to pass time: children's books and strips, swimming and going to the sauna, dreams and their meanings, various kinds of divination (no, I'm not a believer :-)), looking into the night sky, roaming through the Second Colour Maze (which to me looks a bit like the 4004), reading the occasional science fiction, playing the occasional computer game, collecting dice (only two to go!), folk dancing (fondly remembering Praznik), modern dancing and recently some Argentinean tango, gliding (once, for a week, but I'd like to do it again one day), typography and fonts, scanning books (like Teirlinck's Flora Magica), studying color (there is a ColorChecker on my desk), and I'm thinking of learning wall climbing (those climbing walls are so very beautiful) or maybe aikido. However, I spend most of my actual time behind the computer, in the train (there and back again takes four hours) and in bed.

A couple of my friends are on the net (if you happen to meet one of them say "hi" from me). They are: ace, Albert, .:, Andrea, Andrzej, Arno, Barbara Lanara & her Branko, Bas, Bob, bryk, Dan, Désirée, Dimitri, Giel, Hans & Willeke, hansm, Henk, Herman, Hiram, Jan Truijens, Jan Zwanenburg, Jean-Christophe, J$, jeshum, Jesse, John Harrison, John Tromp, Karin, Karst, Luís, Marc, Marco, Marijn, Marina, Marjolein & Sophie & Emma & Hein (pronounced like "Hine") & Piet & Lotta & Annebeth, Mark van Atten, Mark de Does, Mark Meuwese, Martine, Maureen, Michael (author of the MathXpert program), Michiel & Tessa, Mik, Milad, Oop & Fuchsen, Patricia, Paul, Pluk, Sjoerd, Sjouke, sterre, Tigran, Wieb, Wouter & Tine, X and Xander.

*

[do's au)tw=| triw'bolon] Recently I reread the first book of the Elements (and found interactive and colorful versions on the web and also looked at its Greek original.) Those people who think that the input of the current crop of proof checkers (like Mizar) is not very accessible should study Euclid: it's so similar in its formalistic style of homogeneous "code" that it's frightening.

For those who like huge expressions: In 1999 't Hooft and Veltman won the Nobel price for physics and to celebrate I bought Veltman's Diagrammatica. To my delight it turned out to contain the full Lagrangian of the standard model which I copied here (for fun I colored the QED terms red.) Unfortunately Veltman uses imaginary time which is practical but ugly (contraction of same height indices, it hurts the eyes.) Fortunately he gives a recipe to translate to real time, which I tried to apply. I don't know whether I got this all right: I'd like to be notified of errors. Also, note that the neutrinos are massless: this might not be realistic.

To celebrate the millennium, I calculated the number of seconds between the time point between 1 BC and 1 AD and the time point between 1999 and 2000: that turned out to be 63082368022 seconds. (Because the earth rotation slows down and there haven't been leap seconds before 1972, if you go back that many seconds it will be about 2.3 hours before midnight: the 24 hour clock is not accurate at that scale.)

For a long time I have wanted to make an exponential map of the world and finally I have done so. It's a formal version of the famous drawing "A View of the World from Ninth Avenue" by Saul Steinberg (and its local variations). I did another one based on one of NASA's Blue Marble pictures. This one takes the logarithm of the distance along the surface of the earth as the y-coordinate: it's not conformal near the Antipathies but it looks reasonable. The projection of these maps is the complex exponential (see for a thorough explanation these papers) and it uses my apartment as the center of the world. . I also transformed the gifs from powers of ten but that was a bit disappointing, although if you look closely the top half resembles Mario Juric's diagram of the universe as well as its xkcd version.

A nice game you might like to play: suppose you have to go to a place like a home for the aged where you are only allowed a single shelf of books. What books would you bring?

I have discovered that poetry, philosophy and religion is about the same thing, as all three subjects give me exactly the same puzzled feeling of "what is it, that those people want?" Apparently I miss the gene for poetry appreciation, philosophical argument and the experience of God. (I say "I miss the gene for poetry" but I have to admit that I like little songs like Iene Miene Mom.) About my religious feelings, they are something like "dead is dead, gone is gone" ("dood is dood, weg is weg").

Here is a little implementation in ocaml of the untyped lambda calculus. I know there are many similar implementations (like the one in Larry Paulson's ML book) but this is a minimalistic one, in the spirit of HOL Light. It says things like: 

# nf "ISIS";;
- : term = term "^z.z^yz'.zz'(yz')"

I didn't optimize it in any way. I hope it's bug-free. (Recently I added some features for Jan-Willem Klop. Now it can be compiled as a stand alone program, but the code is much messier.)

One would like a formal math system to be able to calculate numerically. If one defines the number pi, then it would be nice if the system could approximate it automatically to something like 3.14 or 3.15 in a reasonable time. HOL Light's REALCALC_CONV almost can do this, as it can calculate: 

#REALCALC_BASE_CONV `exp(&1)` (Int 10) (Int 24);;
it : thm = |- abs (&2718281828459045235360288 - &10 pow 24 * exp (&1)) < &1

(but it doesn't know about arctan so it can't calculate pi; however in John's Intel work there exists a rule called PI_APPROX_RULE that certainly can.) Of course if you don't need to have proofs then calculating pi is easy. That's even true in Coq. (Speaking of Coq: I recently made a silly Coq term. Or, for who does not know Coq, here is a Mizar translation.)

And a short shameful confession: I no longer believe in the standard natural numbers. I don't know exactly what it is that I do believe, but I don't believe that something like the standard natural numbers exist. I shouldn't have tried to study logic: it destroyed my faith. (And then Albert told me it's consistent to suppose that the models of set theory all have non-standard internal natural numbers, thus confusing me even more :-)) But of course I do believe something. For instance, I believe that some kind of natural numbers exist. Of course! Because otherwise nothing would be. There are lots of natural numbers, actually... but only all kinds of non-standard ones.

(gray-on-black style stolen from Hiram; last modification 2017-06-09)

[ik ga ipsen]