Skip to Content »

Michi’s blog » archive for August, 2007

 Coq and simple group theory

  • August 5th, 2007
  • 9:15 pm

Trying to make the time until my flight leaves tomorrow go by, I played around a bit with the proof assistant Coq. And after wrestling a LOT with the assistant, I ended up being able to prove some pretty basic group theory results.

And this is how it goes:

Section Groups.

Variable U : Set.
Variable m : U -> U -> U.
Variable i : U -> U.
Variable e : U.

Hypothesis ass : forall x y z : U, m x (m y z) = m (m x y) z.
Hypothesis runit : forall x : U, m x e = x.
Hypothesis rinv : forall x : U, m x (i x) = e.
 

This sets the stage. It defines a group as a group object in Set, but without the diagonal map. It produces a minimal definition – the left identity and inverse follow from the right ones, which we shall prove immediately.

 Politics and absences

  • August 4th, 2007
  • 8:21 pm

First off, Alexander Borovik has been writing a couple of times about a REALLY nice-sounding mathematical village in Turkey.

And it turns out, the village got closed this summer, with the government officials citing “education without permission” as their reason to close it.

Alexander is sending a petition to the prime minister. You should sign it.

In other news, I’m currently just waiting for Monday to come along. Why Monday? Because that’s the day I’m going back to Stockholm again. Once there, I’ll spend a couple of weeks spending time with friends and family, and then I will go and vow fidelity and those other things. The 25th of August, in case you’re about to ask.

All in all, this means that posting will be sparse if existent until mid-September – when I arrive, fresh out of my honeyforthnight, to Sydney; where the Magma research group host me for some 5-odd weeks. There I expect to have office space, an internet connection and a computer.

 Advertising policy

  • August 1st, 2007
  • 4:38 pm

Today I received an email kind of convincing me that my blog gets seen. It offered me $35 to put up an add for a phone service on one of my old blog posts.

What differentiated this offer from all other spam I get was that it was actually written well enough, and tailored enough, that I believe this guy would even go through with it. Only …

I am not interested.

I run this blog because I like running it. I do system admin myself too. The domain name is mine since my family wants it, and my parents chip in. The net connection also is something that the family chips in on, and is handled without significant cost.

All in all, I do not NEED ads to keep this place up and running.