Performance of models for formalisation

Stream: Machine Learning for Theorem Proving

[Archie Browne]

Hi all, I am interested in hearing about your experiences in using various language models for formalisation (GPT-5, Opus 4.1, DeepSeek-V3, Kimina, Grok etc...). Which have you found most capable? Are they something you commonly use in your work with formalisation? In particular, if a model has shortcomings, what are they? Are there certain areas of Mathematics that are easier for specific models? Most of all it would be good to hear about their performance on research Mathematics. Any concrete examples would be fantastic. Thanks.

[(deleted)]

Rumor has it that GPT-5 with GitHub Copilot is very good

[West]

#lean4 > Vibe Proofing

Cross posting my experience.