About me

I write software to earn money and machine verifiable proofs for fun (see my project IsarMathLib – a library of formalized mathematics for Isabelle/ZF).

Sometimes I write software for fun. I wouldn’t mind writing machine verifiable proofs for money.

You can contact me at user++”@yahoo.com” where user=”skokodyn”.


3 Responses to “About me”

  1. Jesse Alama Says:

    Nice blog! I’m a formal mathematics guy, too, so I’m pleased to come across this resource. I notice that this blog seems to exclude MIZAR, another system for formal mathematics. Their homepage is http://mizar.org; consider tracking it, too (though of course you are welcome to ignore whatever you want — if you want this to be an Isabelle-centric blog, that’s fine.)

  2. slawekk Says:

    I certainly don’t exclude Mizar and I am surprised you have got such impression. I write about Mizar quite often on this blog, things like “Mizar is still the best tool for a mathematician to do formalized mathematics”, “leading proof assistants – HOL Light and Mizar“.

  3. Jesse Alama Says:

    Oh, thanks for clarifying. I got this impression because you didn’t mention mizar or any of it’s recent releases on the front page, unlike Isabelle. I certainly agree with your assessment of mizar :->

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: