Archive for February, 2007

Mizar: automatically verifiable mathematics

Monday, February 26th, 2007

If you are interested in the idea of using computers for verifying the correctness of mathematical proofs, you should check out the Mizar Project. Their language and software allows to express and relate mathematical statements such that proofs can be build in a formally consistent manner. It is all founded upon Tarski-Grothendieck set theory which is, if I understand it correctly, equivalent to axiomatic set theory and first-order logic. Their library currently includes quite a broad number of proofs, including one for Jordan curve theorem.

The attraction of such a system is of course the power that it can give us in finding proofs and checking them automatically. Unfortunately it seems that we have still some distance to go, before most of today’s mathematics can be manipulated and constructed as easily in this system as we currently do on paper and let humans fill in the logical gaps. I do not have real experience with the system, but I gather that the overhead still feels as too much for most people that would not mind putting a stronger and automatically verifiable foundation underneath the theorems they work with. A possible solution would be an interface that allows mathematicians to work with the mathematics at the level they are reasoning, and have the computer fill in the logic connections to and within the lower levels automatically. I’m not sure how feasible this is, but it would be a very significant development if we would obtain such an extension to the system.

Another project that definitively deserves mentioning is the Hilbert II project, initiated by Michael Meyling. This project specifically has the idea I described at the end of the previous paragraph as a goal. If you want to learn more about automatic theorem provers and formalised mathematics with computer programs, check out this talk of Freek Wiedijk or his website.

Seeing the world in four colours

Friday, February 23rd, 2007

Have you ever thought about our perception of the world? Most people think that they are seeing reality, but in reality they perceive sensory input on a small window of the electromagnetic spectrum. We are not seeing ‘everthing there is to be seen‘, but only a portion of it. Furthermore the result is interpreted, so we must be careful with the assumption that what we experience actually exists in a single, unique state that is identical for anyone who perceives it.

Most of us have heard of the various types of colour blindness. Those people experience the same world as we do, but yet different. On the other hand exists the phenomenon of tetrachromacy, a condition that some people, in particular females, have that makes them experience the world in four colours, instead of the usual three. That means that they see (subtle) differences between colours that you as a trichromat experience as identical. And according to this artical on colour vision, pigeons even trump that, being pentachromats and thus discerning five base colours.

The flora and fauna of Ascension

Sunday, February 18th, 2007

Relatively near St. Helena, the island of Napoleon Bonaparte’s second exile, lies Ascension island. Famous scientist Charles Darwin passed the island on one of his journies and described it as barren with very few plants. Today, less then two centuries later, part of the island has become covered with a tropical rainforest through various ad-hoc planting efforts and scientist have been surprised by the speed at which this complex ecological system has developed. Even though the flora and fauna are now richer than before, not everyone agrees that this has been an unequivocal positive transformation; at least four native species have become extinct and others have become endangered.

Most people probably feel that the complex forrest is an improvement over the previous sparse vegetation. This touches once again upon the question whether we should actively try to control and change our environment or to leave everything unchanged as much as possible. And what part of the latter goal of leaving everything unchanged have we already missed by going from a population of 2 million to one of over 6 billion? I think that the lesson to be learnt from Ascension is that change will favor some life and it will kill others. As human beings we should be prudent to strive for change, in particular when we do not fully understand all the factors involved, since at every turning point there is the chance of us ‘becoming out of favor‘.

Invention or discovery?

Friday, February 16th, 2007

Nobody claims that the American continent has been ‘invented‘ by Columbus, or by whomever was first to set foot on the New World. He clearly discovered it, since it was already lying there when he sailed out and, as he was looking for a new route to Asia, he did not even aim to end up there thus only by chance did he learn of the new continent.

From this we conclude that there are at least two factors that influence our idea of what constitutes a discovery as opposed to an invention:

  1. If something already exist and you learn about its existence by mere encounter, then we call it a discovery. An invention on the other hand is about creating something new, something that did not exist before.
  2. Inventions do not happen by chance, since it requires thought and creativity. Furthermore, they tend to solve some specific problem; inventions have purpose. If something was encountered by chance, then in exactly that state, it can only be a discovery. On could say that Australia was discovered and then the British ‘invented’ the continent as a penal colony.

Based upon these observations, can we decide the following question:

Has mankind discovered or invented mathemathics?

Note that there is no definitive answer to this question. The problem is strongly related to the semantics of our language and completely ’solving it’ is not our intention. We take it for a philosophical question, one where our answer tells us more about how we view ourselves (mankind) and the universe we live in, rather than pertaining to some kind of absolute truth.

I used to be convinced that mathematics could only be called a discovery. The intricacy and beauty of all the constructs made me decide that it had to exist outside of human conciousness as well. Since we only came across something that was already there, it cannot be discovery.

Nowadays my conviction has weakend: maybe parts of mathematics really are ‘just an invention’. We try to solve problems and use mathematics for structuring our thoughts. Some problems can be solved in a multitude of ways and people working independently often have found their own but different solutions. All of our mathematics are ultimately based on the axiomatic framework we chose to work from, but even that framework is not universally agreed on by all.

We have barely touched the surface of the discussion, but because of time constraints I’m already going to conclude: mathematics has aspects of both invention and discovery. If we were ever to encounter an intelligent alien race, it would be nice to compare the mathematics they have built, if any, with ours. If it turns out that all concepts of developed and complex areas in mathematics translate one-to-one to each other, I would see that as an indication that those parts of our mathematics, at least in the context of this universe, have an instrinsic nature and thus can only be discovered, not invented.

Science with applications to Hollywood

Monday, February 12th, 2007

Check out the home page of Ron Fedkiw at Stanford University. It has many nices movies and they are all the result of scientific research in some sense.

You might never have realised it, but most of the special effects that are digitally added to movies require some hefty mathematics. How do they visualise a large cruise ship hitting a bridge or Godzilla’s tail taking out part of a building? They simulate the event and calculate what approximately happens. There is one big difference though between simulations for Hollywood and those outside: in Hollywood they only need the results to look accurate to the eye of the average person in the movie theater, whereas others usually want real physical accuracy. Hollywood can thus use other, in particular faster, methods for their simulations.

Note that not all effects are purely digitally added. A lot of images come from real simulations only with small scale models. Digital simulation, however, is getting more popular because of the flexibility it gives us. With current advances in computer hardware and the techniques developed by people like Ron Fedkiw, the simulations are getting faster and faster. This causes a shift to less simulations with scale models and more with the computer. For instance, the computer simulation allows to generate a sequence from any camera viewpoint even ones that are impossible in the physical world. Also, when the creative director want to try a slightly different animation, it is easier to just tweak a few simulation parameters and recalculate the result then to rebuild a whole physical setup and redo the experiment.

An intriguing problem (updated)

Friday, February 9th, 2007

From the thesis of Dafna Talmor, Well-Spaced Points for Numerical Methods (1997):

It is reasonable to conjecture that every well-spaced point set can be tetrahedralized to form a good aspect ratio mesh. However, the Delaunay tetrahedralization fails to oblige us in that respect. Currently, it is unknown if such a tetrahedralization algorithm exists, or if there exists a counter-example: a well-spaced point set with the property that none of its tetrahedralizations is of bounded aspect ratio.

This is probably hard to understand for most of you due to lack of familiarity with the subject. Let me try to provide a translation:

1. There are two kinds of point sets, namely those that are well-spaced and those that are not. Intuitively well-spacedness means that the points are distributed evenly over space. No two points are too close together and there are no gaps. In a crate of oranges the points formed by the centres of all oranges are well-spaced.

2. Delaunay is a criterion for completely triangulating a point set. Applying Delaunay we get a triangulation of any collection of points. When we apply Delaunay to a two-dimensional point set (points in a plane) then, in the case of well-spaced points, we get a triangulation that consists only of ‘voluminous’ triangles, that means triangles that are not arbitrarily flat. In three dimensions, however, a Delaunay triangulation of well-spaced points can contain highly flat tetrahedra (three-dimensional triangles; a pyramid with a triangle instead of a square as bottom face).

3. The Delaunay triangulation is not the only triangulation that is possible. In fact, the possible number of triangulations for a point set is usually very, very large. In the Delaunay triangulation of well-spaced points in 3D only relatively few tetrahedra are flat and with some manipulation they can often be removed by slightly changing the connectivity of the points. If that does not work then points can be moved around a little or even points can be added to remove the flat tetrahedron.

4. What Talmor remarks, and what I recently came across myself, is that is unknown if it is always possible to remove the flat tetrahedra from a Delaunay triangulation of well-spaced points by changing the connectivity. The huge number of possible triangulations makes it unfeasible to try them all. There are two possibilities:

  1. For some well-spaced point sets there is just no triangulation possible that does not contain a flat tetrahedron.
  2. Every well-spaced point set has at least one triangulation without flat tetrahedra. Talmor says that this option is ‘reasonable to conjecture‘ and I concur. However, if such a triangulation is always possible, that leaves us hanging with one big and obvious question:

Is there are algorithm that produces a triangulation without flat tetrahedra, without trying all possible combinations of triangulations?

That sure is a vexing issue.

I imagine that at this point some of you still do not understand the gist of the question. If I find time, I will add some pictures to illustrate some of the concepts.

My interest in this problem is not to solve the issue all together. I’m just interested in creating good triangulations, without flat tetrahedra that is. What I would like to have is an algorithm that for a well-spaced point set produces the triangulation in which the flattest tetrahedron, is more voluminous than the flattest tetrahedra of all other triangulations. Otherwise fomulated: if we measure the quality of a triangulation by the flattest tetrahedron in contains, then we want to find the triangulation with the highest quality that is possible for a particular point set.

It is obvious that Talmor’s problem and my problem relate: assuming that a triangulation without flat tetrahedra always exists, then the optimal triangulation would surely offer an example of such a triangulation.

update: I recently discovered that in the paper Sliver Exudation (2000) it is proven that a triangulation without slivers does indeed exist, if the points have a ‘nice enough’ distribution to begin with. I’m not sure whether their sliver exudation algorithm can actually find the (approximate) optimal triangulation. At least it can find a triangulation without slivers, though the theoretical guarantueed quality is very small.

Welcome to the MMFATI blog!

Monday, February 5th, 2007

Welcome to this new experiment of mine: a thought inspiring blog. The idea is to have something published every monday morning and friday afternoon, so people can warm up for or wind down from their working week with some stimulating thoughts.

I have not figured out for what audience I want to write exactly. In the first place I’m writing for myself, but stimulating the thoughts of other people is important to me as well. My initial thought is that the topics should be comprehensible, at least at a global level, for a broad audience. Also, I’d like to incorporate topics that in some way relate to my own research.

Coming up with something twice a week is a hefty challenge. Please forgive me if a miss my goal. I should be able to come up with at least a single interesting link for each post, but I’m not averse of input by others: if you have an interesting link or topic, please let me know so I can share it here again and reach even more people.

I might not be an expert on every topic I choose to discuss. Actually it is very likely that I’m not an expert in most of the topics I choose to discuss. Please share your critical thoughts and ideas. This blog should not be about me or any single person for that matter, but about sharing ideas, stimulating thoughts and learning. Though this blog is in English, let the lack of English writing skills not stop you from commenting: Dutch is readily understood by myself and, I expect, most of my audience.

Another thing: this blog supports formulas in \LaTeX! That means I can insert nice-looking mathematical terms and equations once in a while! See for yourself, the famous Eulerian identity:

e^{i\pi}=-1.

In case you did not know, the i in this equation equals \sqrt{-1}. Yep, even though they might have told you the opposite in high school, it is possible to take a root from a negative number. One way to interpret this equation is that a rotation of 180 degrees (=\pi) over the unit circle brings you from 1 (=e^0) to -1 (=e^{i \pi}).

Lastly: off course it is not very cool to use the default style for your blog. Changing this is on my TODO-list, but it does not have first-class priority.

Historic note: this blog existed briefly as a science-oriented blog. I quickly realised that the audience that would be interested in that original scope would probably a subset of those of the current scope. Also it should make my task of coming up with new entries easier because now I can write about virtually anthing as long as it can be interpreted in some twisted or perverted way as intellectually interesting. I hope the blog does not devolve into something vulgar and easy, but only time can tell.

Matthijs Sypkens Smit