We have AI at home… › A pleasant surprise [01AT]

I was preparing for my chalk talk when I realised that I could not remember the details of the proof of the main result and they couldn’t really be reconstructed from the abbreviated proof in the paper.

Luckily, I had actually formalised this result in Agda! I did not mention my formalisation in the paper because I do not think of formalisations as scientific contributions except in certain cases (that is a conversation for another day). But I did indeed formalise it because the proof was subtle enough that I needed computerised assistance back when I proved it the first time. The result I obtained was frustratingly weak, and seemed to require some annoying side conditions in order to go through; the formalisation helped me be certain that these side conditions were in fact sufficient.

Anyway, I was messing around with the code and what I realised was that I had missed a trick back then: one of the side conditions was actually unnecessary, and it seems kind of likely that the other one is unnecessary too. I am certain I would not have noticed this if I hadn't had the proof assistant, which made it easy for me to try something out and see if it worked. I should have time to update the paper to claim the strong result prior to the LICS camera-ready deadline next month.