So for whomever is reading this page. This is my very first web page on which I will be recording my progress of my masterthesis and whatever problems I run into. I am specifically putting this on this web page with 3 different reasons:

  • I noticed during the writing of my bachelor thesis that it is rather nice to actually always inform my supervisors what I have been working on (I did it via e-mail that year);
  • This time I might be working together with supervisor, but possibly also other researchers. Thus in order to also inform them on what I have been working on.
  • To have a nice way to read back on what I had worked on at specific points, so that I can possibly show during the presentation of my master thesis what I was working on at what time. I will probably regret this decision later on, but for now it is more than a little nice to just jot down my (non-intrusive) thoughts.

Anyway this week I have mostly started reading this thread on the lean zulipchat and of course setting up this thesis.

It was already nice to know that there are a bunch of people now that are interested in formalising some form of quantum computing algorithms in Lean and importantly, that this is also not a trivial task to do in a nice way: The trade-off between the most general case of infinite dimensional circuits versus the specific case of finite dimensional circuits is apparently big enough that it isn’t completely clear what the best choice here is.

Similarly it is to a certain extent sad that there is still no proper direction chosen on where, and how, to formalise quantum algorithm. Specifically to what extend we will try and put theorems “upstream” in physlib/mathlib versus in CSlib, which if I understand it correctly seems to be the home where we will actually work on the specific algorithms.

Also reading through some of the posts in the thread it was interesting to see that probably the best way to write these algorithms is using monads, just like is the “natural” way of writing stateful functional programming languages (which Lean belongs to). This was something I did expect, but still to see it in action is fun to say the least.

To end, after having written my first blogpost let’s get to talking about writing my thesis, or more aptly what boundaries I think I will set for myself. At first I wanted to look into using agentic AI to formalise theorems, but the longer I am considering that the more I am thinking that I will probably not like that. Compared to my bachelor thesis wherein (probably to my detriment) I did not use AI in anyway whatsoever, I will at least plan on using on the UvA’s AIChat. Mostly to look up how to do x,y or z in Lean which I didn’t yet know about. I think I am very much at the stage of learning LEAN that using LLMs for look up is moreso to get introduced to new methods to improve/shorten my LEAN code than letting the computer solve the problems for me 1. It will be sad to leave my AI-free hermit life after me though :’(.

  1. At the very least I hope so. In my bachelor thesis’ code I wrote down wayyyy too many apply? to get possibly further + using the creation of a lot of short rewrite hypothesis and then using simp. At least after having learned show_term I now know how to already clean up a lot of this code. ↩