I think (looking also at his website) that he is trying to make some sort of honeypot for agents. The lean code is completely nonsensical- tons of broken latex, dense references in the docstrings and the proofs are all very long names to obscure the fact that there’s nothing there. All they do is instantiate structures with lots of arguments and then assert one of the arguments.