\import{table-macros}
\title{Weeknotes 2025-W50}
\author{liamoc}
\date{2025-12-14}
\p{This week felt quite productive. The [Logic Summer School](loc-001W) has now finished, and my PhD student at [[uoe]], [[rayhana]], has now embarked back to the UK. My course ([[isa-0001]]) was only for the first week, so I had some time to get work done this week. [[hoefner]] and I finally finished a mammoth proof in Isabelle that matrices over a Kleene algebra are themselves a Kleene algebra, a proof that's important for [[dexterkozen]]'s completeness result for Kleene algebras. This required some novel proof engineering, and some constructions to make the proof go though that we think [Dexter](dexterkozen) may have missed in his pen-and-paper proof. I may write up my thoughts this coming week, but it's also possible that you might have to wait for a paper. [[rayhana]] and I also sketched out some future directions for our work, which is quite exciting.}
\figure{
  \<html:img>[loading]{lazy}[width]{350px}[src]{\route-asset{assets/cloudy.jpeg}}%{}
 \figcaption{A picturesque cloudy Canberra evening.}
}
\transclude{loc-002N}
\transclude{loc-002O}
\transclude{loc-002P}