On: Show HN: Formal – Formal verification for AI-generated code using Lean 4

[yamafaktory]

I'm sorry if it was unclear. My comment was just a validation of your assertion. It does use Claude - or any openai compatible LLM - to perform the extraction.