I'm a mathematician and I'm not sure one should believe those results right now.. An automatic formalization requires a system of logic rules to be applied, which is not something LLMs are great at (remember the Apple paper a while ago?). I'm very curious to see how the community will react after the initial hype.. so far, it's being quite disappointing..
The LLM is not the thing applying the logical rules. That is instead the deterministic system Lean 4. (Also that Apple paper was garbage even when it was written, assuming you’re referring to The Illusion of Thinking, and LLMs have got much better since.)
Kevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interactive theorem proving for quite some time. The difference now: if you don't adapt, you are obsolete and done for as a mathematician.
