Autoformalising Wiedijk's #40

[Xander Mackay]

I'm currently working on an autoformalisation of Minkowski's Fundamental Theorem, #40 of Wiedijk's 100. I'm using Claude Code, and it seems to be making good progress so far.

Should I just follow the usual set.mm contribution guidelines, set up my own mathbox and so forth? Have there been any significant AI-assisted formalisations recently, or is this something new that there isn't really a policy for yet?

I figure I'll start by putting it in my own mathbox, and attribute each theorem as: "Contributed by Xander Mackay and Claude".

Cheers,

Xander Mackay