Michi’s blog » archive for August, 2007

Coq and simple group theory

  • August 5th, 2007

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.

This is a preview of Coq and simple group theory. Read the full post (860 words)

Politics and absences

  • August 4th, 2007

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.

This is a preview of Politics and absences. Read the full post (169 words)

Advertising policy

  • August 1st, 2007

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.

This is a preview of Advertising policy. Read the full post (229 words)

post navigation
about
Michi is a PhD student working in homological algebra. This blog is his outlet for texts with some manner of thought put into them. Over at his LiveJournal intimate details and streams of consciousness might be found.
Not all here is mathematics. All here, though, are my personal thoughts and opinions. Please read the about page (linked above) for more details.
This blog uses statcounter.com for logging and traffic analysis. In order to identify return visitors, this site will issue a cookie on viewing the blog.
buttons

latest comments
search
blogs and links
the rdc* theme