Comment by empath75

If you have ever worked with claude code and lean, it goes back and forth between lean and NL reasoning. I have done a few proofs with claude and it almost _never_ gets the argument right in prose. It usually has to go into lean and grind through proof obligations and then it finds problems, work arounds etc.