Comment by zozbot234
2 days ago
> I don't believe that's what's happening in this specific example (and am probably wrong), but this is where a lot of Tao's enthusiasm lies.
It absolutely is. With the twist that ChatGPT 5.2 can now also "explain" an AI-generated Lean proof in human-readable terms. This is a game changer, because "refactoring" can now become end-to-end: if the human explanation of a Lean proof is hard to grok and could be improved, you can test changes directly on the formal text and check that the proof still goes through for the original statement.
Thank you, I had corrected it earlier when I had some time to further investigate what was happening.
Formal verification combined with AI is, imho, exactly the type of thinking that gets the most value out of the current state of LLMs.