3 ms·

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

• sjdv1982 6mo ago
  I was initially very excited about this, but looking at the code: https://github.com/yamafaktory/formal/blob/4f95787ceeabb0f0961d5122c7f9b768a22f4993/feature_extractor.py#L75 https://github.com/yamafaktory/formal/blob/4f95787ceeabb0f09... To extract properties to verify... you call Claude??
  • yamafaktory 6mo ago
    Well, I can understand your frustration, but this is basically a pipeline that takes some code written by an LLM and attempts to prove its correctness using the Lean 4 theorem prover.
    • sjdv1982 6mo ago
      How does your reply relate to my comment?
      • yamafaktory 6mo ago
        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.
  • deleted 6mo ago
    [deleted]
• angarrido 6mo ago
  [dead]