Another proof (AI-generated with human guidance) of Hilbert-Smith, together with complete Lean4 formalization (100k LOC), on which I have worked independently over the last few weeks in my free time. It’s the first Lean4 formalization available afaik, since openai didn’t publish it. Planned on cleaning it up, but had to rush it out after openai’s release. You don’t need the latest biggest models to do new research (but it helps).